--- a/TFL/post.ML Mon Jun 19 19:56:32 2006 +0200
+++ b/TFL/post.ML Mon Jun 19 20:21:30 2006 +0200
@@ -170,7 +170,9 @@
| tracing false msg = writeln msg;
fun simplify_defn strict thy cs ss congs wfs id pats def0 =
- let val def = Thm.freezeT def0 RS meta_eq_to_obj_eq
+ let
+ val ([def1], _) = Variable.importT [def0] (Variable.thm_context def0);
+ val def = def1 RS meta_eq_to_obj_eq;
val {theory,rules,rows,TCs,full_pats_TCs} =
Prim.post_definition congs (thy, (def,pats))
val {lhs=f,rhs} = S.dest_eq (concl def)