src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML

   | freeze (Var ((s, _), T)) = Free (s, freezeT T)
   | freeze (Const (s, T)) = Const (s, freezeT T)
   | freeze (Free (s, T)) = Free (s, freezeT T)
   | freeze t = t
 
-fun goal_of_thm thy = Thm.prop_of #> freeze #> Thm.cterm_of thy #> Goal.init
+fun goal_of_thm thy = Thm.prop_of #> freeze #> Thm.global_cterm_of thy #> Goal.init
 
 fun run_prover_for_mash ctxt params prover goal_name facts goal =
   let
     val problem =
       {comment = "Goal: " ^ goal_name, state = Proof.init ctxt, goal = goal, subgoal = 1,