src/HOL/Tools/Function/size.ML

       let
         val (Free (c, _), rhs) = (Logic.dest_equals o Syntax.check_term lthy) eq;
         val (thm, lthy') = lthy
           |> Local_Theory.define ((Binding.name c, NoSyn), ((Binding.name def_name, []), rhs))
           |-> (fn (t, (_, thm)) => Spec_Rules.add Spec_Rules.Equational ([t], [thm]) #> pair thm);
-        val ctxt_thy = ProofContext.init_global (ProofContext.theory_of lthy');
-        val thm' = singleton (ProofContext.export lthy' ctxt_thy) thm;
+        val ctxt_thy = Proof_Context.init_global (Proof_Context.theory_of lthy');
+        val thm' = singleton (Proof_Context.export lthy' ctxt_thy) thm;
       in (thm', lthy') end;
 
     val ((size_def_thms, size_def_thms'), thy') =
       thy
       |> Sign.add_consts_i (map (fn (s, T) =>

       ||>> fold_map define_overloaded
         (def_names' ~~ map Logic.mk_equals (overloaded_size_fns ~~ map (app fs') rec_combs1))
       ||> Class.prove_instantiation_instance (K (Class.intro_classes_tac []))
       ||> Local_Theory.exit_global;
 
-    val ctxt = ProofContext.init_global thy';
+    val ctxt = Proof_Context.init_global thy';
 
     val simpset1 = HOL_basic_ss addsimps @{thm Nat.add_0} :: @{thm Nat.add_0_right} ::
       size_def_thms @ size_def_thms' @ rec_rewrites @ extra_rewrites;
     val xs = map (fn i => "x" ^ string_of_int i) (1 upto length recTs2);