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