src/HOL/Tools/Meson/meson.ML

   val spec_varT = Thm.typ_of_cterm spec_var;
   fun name_of (Const (@{const_name All}, _) $ Abs(x,_,_)) = x | name_of _ = Name.uu;
 in  
   fun freeze_spec th ctxt =
     let
-      val cert = Proof_Context.cterm_of ctxt;
       val ([x], ctxt') =
         Variable.variant_fixes [name_of (HOLogic.dest_Trueprop (Thm.concl_of th))] ctxt;
-      val spec' = Thm.instantiate ([], [(spec_var, cert (Free (x, spec_varT)))]) spec;
+      val spec' = spec
+        |> Thm.instantiate ([], [(spec_var, Proof_Context.cterm_of ctxt' (Free (x, spec_varT)))]);
     in (th RS spec', ctxt') end
 end;
 
 fun apply_skolem_theorem (th, rls) =
   let