src/HOL/Tools/Meson/meson.ML
changeset 59617 b60e65ad13df
parent 59586 ddf6deaadfe8
child 59621 291934bac95e
     1.1 --- a/src/HOL/Tools/Meson/meson.ML	Thu Mar 05 13:28:04 2015 +0100
     1.2 +++ b/src/HOL/Tools/Meson/meson.ML	Fri Mar 06 00:00:57 2015 +0100
     1.3 @@ -352,10 +352,10 @@
     1.4  in  
     1.5    fun freeze_spec th ctxt =
     1.6      let
     1.7 -      val cert = Proof_Context.cterm_of ctxt;
     1.8        val ([x], ctxt') =
     1.9          Variable.variant_fixes [name_of (HOLogic.dest_Trueprop (Thm.concl_of th))] ctxt;
    1.10 -      val spec' = Thm.instantiate ([], [(spec_var, cert (Free (x, spec_varT)))]) spec;
    1.11 +      val spec' = spec
    1.12 +        |> Thm.instantiate ([], [(spec_var, Proof_Context.cterm_of ctxt' (Free (x, spec_varT)))]);
    1.13      in (th RS spec', ctxt') end
    1.14  end;
    1.15