changeset 59580 | cbc38731d42f |
parent 59498 | 50b60f501b05 |
child 59582 | 0fbed69ff081 |
--- a/src/HOL/Tools/Meson/meson.ML Tue Mar 03 17:20:51 2015 +0100 +++ b/src/HOL/Tools/Meson/meson.ML Tue Mar 03 19:08:04 2015 +0100 @@ -352,7 +352,7 @@ in fun freeze_spec th ctxt = let - val cert = Thm.cterm_of (Proof_Context.theory_of ctxt); + val cert = Proof_Context.cterm_of ctxt; val ([x], ctxt') = Variable.variant_fixes [name_of (HOLogic.dest_Trueprop (concl_of th))] ctxt; val spec' = Thm.instantiate ([], [(spec_var, cert (Free (x, spec_varT)))]) spec; in (th RS spec', ctxt') end