src/HOL/Tools/Function/lexicographic_order.ML

     fold_rev Logic.all vars (Logic.list_implies (prems, concl))
   end
 
 fun mk_cell ctxt solve_tac (vars, prems, lhs, rhs) mfun = Lazy.lazy (fn _ =>
   let
-    val goals = Proof_Context.cterm_of ctxt o mk_goal (vars, prems, mfun $ lhs, mfun $ rhs)
+    val goals = Thm.cterm_of ctxt o mk_goal (vars, prems, mfun $ lhs, mfun $ rhs)
   in
     case try_proof (goals @{const_name Orderings.less}) solve_tac of
       Solved thm => Less thm
     | Stuck thm =>
       (case try_proof (goals @{const_name Orderings.less_eq}) solve_tac of

                   Pretty.quote (Syntax.pretty_term ctxt relation)])
             else ()
   
         in (* 4: proof reconstruction *)
           st |>
-          (PRIMITIVE (cterm_instantiate [apply2 (Proof_Context.cterm_of ctxt) (rel, relation)])
+          (PRIMITIVE (cterm_instantiate [apply2 (Thm.cterm_of ctxt) (rel, relation)])
             THEN (REPEAT (rtac @{thm "wf_mlex"} 1))
             THEN (rtac @{thm "wf_empty"} 1)
             THEN EVERY (map prove_row clean_table))
         end
   end) 1 st;