[isabelle] exception using "case ... of ..." with HOLCF



Dear all,

when I tried to adapt Isabelle/HOLCF Prelude (e.g.,

  hg clone http://hg.code.sf.net/p/holcf-prelude/code holcf-prelude

) to Isabelle2013-2-RC3 I got an exception in the definition of

  fixrec scanr :: "('a → 'b → 'b) → 'b → ['a] → ['b]" where
  "scanr⋅f⋅q0⋅[] = [q0]" |
  "scanr⋅f⋅q0⋅(x : xs) = (
    let qs = scanr⋅f⋅q0⋅xs in
    (case qs of
      [] ⇒ ⊥
    | q : _ ⇒ f⋅x⋅q : qs))"

(and similar definitions). The error message is

  exception TERM raised (line 142 of "Syntax/syntax_trans.ML"):
  binder_tr: _cabs
  \<^const>dummy_pattern
\<^const>Cfun.Rep_cfun (\<^const>Cfun.Rep_cfun \<^const>Data_List.list.Cons (\<^const>Cfun.Rep_cfun (\<^const>Cfun.Rep_cfun f x) q)) qs

What is this supposed to tell me? ;)

cheers

chris




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.