--- a/src/Pure/Isar/code.ML Wed Feb 24 14:34:40 2010 +0100
+++ b/src/Pure/Isar/code.ML Wed Feb 24 14:42:28 2010 +0100
@@ -422,8 +422,9 @@
^ " :: " ^ string_of_typ thy ty');
val _ = Thm.cterm_of thy (Const (rep, ty_abs --> ty)) handle TYPE _ =>
error ("Not a projection:\n" ^ string_of_const thy rep);
- val cert = Logic.mk_equals (Const (abs, ty --> ty_abs) $ (Const (rep, ty_abs --> ty)
- $ Free ("x", ty_abs)), Free ("x", ty_abs));
+ val param = Free ("x", ty_abs);
+ val cert = Logic.all param (Logic.mk_equals
+ (Const (abs, ty --> ty_abs) $ (Const (rep, ty_abs --> ty) $ param), param));
in (tyco, (vs ~~ sorts, ((fst abs_ty, ty), (rep, cert)))) end;
fun get_type_entry thy tyco = case these (Symtab.lookup ((the_types o the_exec) thy) tyco)