[isabelle] getting past ConstDefs.add_constdefs_i



I have a definitional term, of the form 

  Const ("==", ty) $ Free(name, ty') $ tm

such that it certifies with respect to a given theory, thy.

Thus, 

  > cterm_of thy eqt;
  val it =
     "foo_body ==
      TRY \<acute>j :== the (h_val \<acute>the_heap \<acute>i) CATCH SKIP END"
  : Thm.cterm

But, if I try to use this as the basis for a definition, I get an
error from the constant certification part of the code:

  > thy |> Constdefs.add_constdefs_i ([], [(NONE, (("", []), eqt))]);
  Exception-
     TYPE
        ("Illegal type for constant \"mytest.globals.the_heap\" :: globals => addr => word8",
           [],
           []) raised

What am I likely to be doing wrong in my invocation of
add_constdefs_i?

Thanks,
Michael.






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