src/HOL/Tools/Function/termination.ML

     mk_desc thy tac vs Gam l r m1 m2
   end
 
 fun create ctxt chain_tac descent_tac T rel =
   let
-    val thy = ProofContext.theory_of ctxt
+    val thy = Proof_Context.theory_of ctxt
     val sk = mk_sum_skel rel
     val Ts = node_types sk T
     val M = Inttab.make (map_index (apsnd (MeasureFunctions.get_measure_functions ctxt)) Ts)
     val chain_cache = Cache.create Term2tab.empty Term2tab.lookup Term2tab.update
       (prove_chain thy chain_tac)

 
 in
 
 fun wf_union_tac ctxt st =
   let
-    val thy = ProofContext.theory_of ctxt
+    val thy = Proof_Context.theory_of ctxt
     val cert = cterm_of (theory_of_thm st)
     val ((_ $ (_ $ rel)) :: ineqs) = prems_of st
 
     fun mk_compr ineq =
       let