src/HOL/Tools/Function/mutual.ML

     fun inst t = subst_bounds (rev qs, t)
     val gs = map inst pre_gs
     val args = map inst pre_args
     val rhs = inst pre_rhs
 
-    val cqs = map (Proof_Context.cterm_of ctxt) qs
-    val ags = map (Thm.assume o Proof_Context.cterm_of ctxt) gs
+    val cqs = map (Thm.cterm_of ctxt) qs
+    val ags = map (Thm.assume o Thm.cterm_of ctxt) gs
 
     val import = fold Thm.forall_elim cqs
       #> fold Thm.elim_implies ags
 
     val export = fold_rev (Thm.implies_intr o Thm.cprop_of) ags

 
 fun mk_applied_form ctxt caTs thm =
   let
     val xs =
       map_index (fn (i, T) =>
-        Proof_Context.cterm_of ctxt
+        Thm.cterm_of ctxt
           (Free ("x" ^ string_of_int i, T))) caTs (* FIXME: Bind xs properly *)
   in
     fold (fn x => fn thm => Thm.combination thm (Thm.reflexive x)) xs thm
     |> Conv.fconv_rule (Thm.beta_conversion true)
     |> fold_rev Thm.forall_intr xs

 
     val Ps = map2 mk_P parts newPs
     val case_exp = Sum_Tree.mk_sumcases HOLogic.boolT Ps
 
     val induct_inst =
-      Thm.forall_elim (Proof_Context.cterm_of ctxt case_exp) induct
+      Thm.forall_elim (Thm.cterm_of ctxt case_exp) induct
       |> full_simplify (put_simpset Sum_Tree.sumcase_split_ss ctxt)
       |> full_simplify (put_simpset HOL_basic_ss ctxt addsimps all_f_defs)
 
     fun project rule (MutualPart {cargTs, i, ...}) k =
       let
         val afs = map_index (fn (j,T) => Free ("a" ^ string_of_int (j + k), T)) cargTs (* FIXME! *)
         val inj = Sum_Tree.mk_inj ST n i (foldr1 HOLogic.mk_prod afs)
       in
         (rule
-         |> Thm.forall_elim (Proof_Context.cterm_of ctxt inj)
+         |> Thm.forall_elim (Thm.cterm_of ctxt inj)
          |> full_simplify (put_simpset Sum_Tree.sumcase_split_ss ctxt)
-         |> fold_rev (Thm.forall_intr o Proof_Context.cterm_of ctxt) (afs @ newPs),
+         |> fold_rev (Thm.forall_intr o Thm.cterm_of ctxt) (afs @ newPs),
          k + length cargTs)
       end
   in
     fst (fold_map (project induct_inst) parts 0)
   end

     val arg_vars = rev arg_vars
 
     val argsT = fastype_of (HOLogic.mk_tuple arg_vars)
     val (args, name_ctxt) = mk_var "x" argsT name_ctxt
     
-    val P = mk_var "P" @{typ "bool"} name_ctxt |> fst |> Proof_Context.cterm_of ctxt
+    val P = mk_var "P" @{typ "bool"} name_ctxt |> fst |> Thm.cterm_of ctxt
     val sumtree_inj = Sum_Tree.mk_inj ST n i args
 
     val sum_elims =
       @{thms HOL.notE[OF Sum_Type.sum.distinct(1)] HOL.notE[OF Sum_Type.sum.distinct(2)]}
 

       REPEAT (eresolve_tac ctxt @{thms Pair_inject Inl_inject[elim_format] Inr_inject[elim_format]} i)
       THEN REPEAT (eresolve_tac ctxt sum_elims i)
   in
     cases_rule
     |> Thm.forall_elim P
-    |> Thm.forall_elim (Proof_Context.cterm_of ctxt sumtree_inj)
+    |> Thm.forall_elim (Thm.cterm_of ctxt sumtree_inj)
     |> Tactic.rule_by_tactic ctxt (ALLGOALS prep_subgoal)
-    |> Thm.forall_intr (Proof_Context.cterm_of ctxt args)
+    |> Thm.forall_intr (Thm.cterm_of ctxt args)
     |> Thm.forall_intr P
   end
 
 
 fun mk_partial_rules_mutual lthy inner_cont (m as Mutual {parts, fqgars, n, ST, ...}) proof =