src/Tools/IsaPlanner/isand.ML

     val fvs = map Free (xs ~~ map snd alls);
   in ((subst_bounds (fvs,body)), fvs) end;
 
 fun fix_alls_cterm ctxt i th =
   let
-    val cert = Thm.cterm_of (Thm.theory_of_thm th);
+    val cert = Thm.global_cterm_of (Thm.theory_of_thm th);
     val (fixedbody, fvs) = fix_alls_term ctxt i (Thm.prop_of th);
     val cfvs = rev (map cert fvs);
     val ct_body = cert fixedbody;
   in (ct_body, cfvs) end;
 

  ["SG0", ..., "SGm"] : thm list ->   -- export function
    "G" : thm)
 *)
 fun subgoal_thms th =
   let
-    val cert = Thm.cterm_of (Thm.theory_of_thm th);
+    val cert = Thm.global_cterm_of (Thm.theory_of_thm th);
 
     val t = Thm.prop_of th;
 
     val prems = Logic.strip_imp_prems t;
     val aprems = map (Thm.trivial o cert) prems;