src/HOL/Library/old_recdef.ML
changeset 60825 bacfb7c45d81
parent 60781 2da59cdf531c
child 60949 ccbf9379e355
--- a/src/HOL/Library/old_recdef.ML	Tue Jul 28 21:31:16 2015 +0200
+++ b/src/HOL/Library/old_recdef.ML	Tue Jul 28 21:47:03 2015 +0200
@@ -2625,7 +2625,8 @@
 
 fun simplify_defn ctxt strict congs wfs pats def0 =
   let
-    val def = Thm.unvarify_global def0 RS meta_eq_to_obj_eq
+    val thy = Proof_Context.theory_of ctxt;
+    val def = Thm.unvarify_global thy def0 RS meta_eq_to_obj_eq
     val {rules, rows, TCs, full_pats_TCs} = Prim.post_definition ctxt congs (def, pats)
     val {lhs=f,rhs} = USyntax.dest_eq (concl def)
     val (_,[R,_]) = USyntax.strip_comb rhs