diff -r 92d7d8e4f1bf -r 291934bac95e src/HOL/Tools/Function/mutual.ML
--- a/src/HOL/Tools/Function/mutual.ML	Fri Mar 06 14:01:08 2015 +0100
+++ b/src/HOL/Tools/Function/mutual.ML	Fri Mar 06 15:58:56 2015 +0100
@@ -158,8 +158,8 @@
     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
@@ -198,7 +198,7 @@
   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
@@ -226,7 +226,7 @@
     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)
 
@@ -236,9 +236,9 @@
         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
@@ -258,7 +258,7 @@
     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 =
@@ -270,9 +270,9 @@
   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