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