clarified context;

--- a/src/HOL/Tools/Function/fun.ML	Fri Mar 06 21:14:27 2015 +0100
+++ b/src/HOL/Tools/Function/fun.ML	Fri Mar 06 21:20:30 2015 +0100
@@ -28,7 +28,6 @@
     fun err str = error (cat_lines ["Malformed definition:",
       str ^ " not allowed in sequential mode.",
       Syntax.string_of_term ctxt geq])
-    val thy = Proof_Context.theory_of ctxt
 
     fun check_constr_pattern (Bound _) = ()
       | check_constr_pattern t =

--- a/src/HOL/Tools/Function/function_core.ML	Fri Mar 06 21:14:27 2015 +0100
+++ b/src/HOL/Tools/Function/function_core.ML	Fri Mar 06 21:20:30 2015 +0100
@@ -228,12 +228,12 @@
 
 (* Returns "Gsi, Gsj, lhs_i = lhs_j |-- rhs_j_f = rhs_i_f" *)
 (* if j < i, then turn around *)
-fun get_compat_thm thy cts i j ctxi ctxj =
+fun get_compat_thm ctxt cts i j ctxi ctxj =
   let
     val ClauseContext {cqs=cqsi,ags=agsi,lhs=lhsi,...} = ctxi
     val ClauseContext {cqs=cqsj,ags=agsj,lhs=lhsj,...} = ctxj
 
-    val lhsi_eq_lhsj = Thm.global_cterm_of thy (HOLogic.mk_Trueprop (mk_eq (lhsi, lhsj)))
+    val lhsi_eq_lhsj = Thm.cterm_of ctxt (HOLogic.mk_Trueprop (mk_eq (lhsi, lhsj)))
   in if j < i then
     let
       val compat = lookup_compat_thm j i cts
@@ -287,8 +287,10 @@
   end
 
 
-fun mk_uniqueness_clause thy globals compat_store clausei clausej RLj =
+fun mk_uniqueness_clause ctxt globals compat_store clausei clausej RLj =
   let
+    val thy = Proof_Context.theory_of ctxt
+
     val Globals {h, y, x, fvar, ...} = globals
     val ClauseInfo {no=i, cdata=cctxi as ClauseContext {ctxt=ctxti, lhs=lhsi, case_hyp, ...}, ...} =
       clausei
@@ -298,18 +300,18 @@
       mk_clause_context x ctxti cdescj
 
     val rhsj'h = Pattern.rewrite_term thy [(fvar,h)] [] rhsj'
-    val compat = get_compat_thm thy compat_store i j cctxi cctxj
+    val compat = get_compat_thm ctxt compat_store i j cctxi cctxj
     val Ghsj' =
       map (fn RCInfo {h_assum, ...} =>
-        Thm.assume (Thm.global_cterm_of thy (subst_bounds (rev qsj', h_assum)))) RCsj
+        Thm.assume (Thm.cterm_of ctxt (subst_bounds (rev qsj', h_assum)))) RCsj
 
     val RLj_import = RLj
       |> fold Thm.forall_elim cqsj'
       |> fold Thm.elim_implies agsj'
       |> fold Thm.elim_implies Ghsj'
 
-    val y_eq_rhsj'h = Thm.assume (Thm.global_cterm_of thy (HOLogic.mk_Trueprop (mk_eq (y, rhsj'h))))
-    val lhsi_eq_lhsj' = Thm.assume (Thm.global_cterm_of thy (HOLogic.mk_Trueprop (mk_eq (lhsi, lhsj'))))
+    val y_eq_rhsj'h = Thm.assume (Thm.cterm_of ctxt (HOLogic.mk_Trueprop (mk_eq (y, rhsj'h))))
+    val lhsi_eq_lhsj' = Thm.assume (Thm.cterm_of ctxt (HOLogic.mk_Trueprop (mk_eq (lhsi, lhsj'))))
        (* lhs_i = lhs_j' |-- lhs_i = lhs_j' *)
   in
     (trans OF [case_hyp, lhsi_eq_lhsj']) (* lhs_i = lhs_j' |-- x = lhs_j' *)
@@ -324,12 +326,13 @@
       (* lhs_i = lhs_j' , y = rhs_j_h' |-- Gj', Rj1'...Rjk' ==> y = rhs_i_f *)
     |> Thm.implies_intr (Thm.cprop_of y_eq_rhsj'h)
     |> Thm.implies_intr (Thm.cprop_of lhsi_eq_lhsj')
-    |> fold_rev Thm.forall_intr (Thm.global_cterm_of thy h :: cqsj')
+    |> fold_rev Thm.forall_intr (Thm.cterm_of ctxt h :: cqsj')
   end
 
 
 
-fun mk_uniqueness_case ctxt globals G f ihyp ih_intro G_cases compat_store clauses rep_lemmas clausei =
+fun mk_uniqueness_case ctxt
+    globals G f ihyp ih_intro G_cases compat_store clauses rep_lemmas clausei =
   let
     val thy = Proof_Context.theory_of ctxt
     val Globals {x, y, ranT, fvar, ...} = globals
@@ -348,7 +351,7 @@
     val G_lhs_y = Thm.assume (Thm.cterm_of ctxt (HOLogic.mk_Trueprop (G $ lhs $ y)))
 
     val unique_clauses =
-      map2 (mk_uniqueness_clause thy globals compat_store clausei) clauses rep_lemmas
+      map2 (mk_uniqueness_clause ctxt globals compat_store clausei) clauses rep_lemmas
 
     fun elim_implies_eta A AB =
       Thm.bicompose (SOME ctxt) {flatten = false, match = true, incremented = false}
@@ -548,11 +551,11 @@
     ctxt')
   end
 
-fun inst_RC thy fvar f (rcfix, rcassm, rcarg) =
+fun inst_RC ctxt fvar f (rcfix, rcassm, rcarg) =
   let
     fun inst_term t = subst_bound(f, abstract_over (fvar, t))
   in
-    (rcfix, map (Thm.assume o Thm.global_cterm_of thy o inst_term o Thm.prop_of) rcassm, inst_term rcarg)
+    (rcfix, map (Thm.assume o Thm.cterm_of ctxt o inst_term o Thm.prop_of) rcassm, inst_term rcarg)
   end
 
 
@@ -594,34 +597,35 @@
 val acc_subset_induct = @{thm predicate1I} RS @{thm accp_subset_induct}
 
 
-fun mk_partial_induct_rule thy globals R complete_thm clauses =
+fun mk_partial_induct_rule ctxt globals R complete_thm clauses =
   let
     val Globals {domT, x, z, a, P, D, ...} = globals
     val acc_R = mk_acc domT R
 
-    val x_D = Thm.assume (Thm.global_cterm_of thy (HOLogic.mk_Trueprop (D $ x)))
-    val a_D = Thm.global_cterm_of thy (HOLogic.mk_Trueprop (D $ a))
+    val x_D = Thm.assume (Thm.cterm_of ctxt (HOLogic.mk_Trueprop (D $ x)))
+    val a_D = Thm.cterm_of ctxt (HOLogic.mk_Trueprop (D $ a))
 
-    val D_subset = Thm.global_cterm_of thy (Logic.all x
-      (Logic.mk_implies (HOLogic.mk_Trueprop (D $ x), HOLogic.mk_Trueprop (acc_R $ x))))
+    val D_subset =
+      Thm.cterm_of ctxt (Logic.all x
+        (Logic.mk_implies (HOLogic.mk_Trueprop (D $ x), HOLogic.mk_Trueprop (acc_R $ x))))
 
     val D_dcl = (* "!!x z. [| x: D; (z,x):R |] ==> z:D" *)
       Logic.all x (Logic.all z (Logic.mk_implies (HOLogic.mk_Trueprop (D $ x),
         Logic.mk_implies (HOLogic.mk_Trueprop (R $ z $ x),
           HOLogic.mk_Trueprop (D $ z)))))
-      |> Thm.global_cterm_of thy
+      |> Thm.cterm_of ctxt
 
     (* Inductive Hypothesis: !!z. (z,x):R ==> P z *)
     val ihyp = Logic.all_const domT $ Abs ("z", domT,
       Logic.mk_implies (HOLogic.mk_Trueprop (R $ Bound 0 $ x),
         HOLogic.mk_Trueprop (P $ Bound 0)))
-      |> Thm.global_cterm_of thy
+      |> Thm.cterm_of ctxt
 
     val aihyp = Thm.assume ihyp
 
     fun prove_case clause =
       let
-        val ClauseInfo {cdata = ClauseContext {ctxt, qs, cqs, ags, gs, lhs, case_hyp, ...},
+        val ClauseInfo {cdata = ClauseContext {ctxt = ctxt1, qs, cqs, ags, gs, lhs, case_hyp, ...},
           RCs, qglr = (oqs, _, _, _), ...} = clause
 
         val case_hyp_conv = K (case_hyp RS eq_reflection)
@@ -629,14 +633,14 @@
           val lhs_D = fconv_rule (arg_conv (arg_conv (case_hyp_conv))) x_D
           val sih =
             fconv_rule (Conv.binder_conv
-              (K (arg1_conv (arg_conv (arg_conv case_hyp_conv)))) ctxt) aihyp
+              (K (arg1_conv (arg_conv (arg_conv case_hyp_conv)))) ctxt1) aihyp
         end
 
         fun mk_Prec (RCInfo {llRI, RIvs, CCas, rcarg, ...}) = sih
-          |> Thm.forall_elim (Thm.global_cterm_of thy rcarg)
+          |> Thm.forall_elim (Thm.cterm_of ctxt rcarg)
           |> Thm.elim_implies llRI
           |> fold_rev (Thm.implies_intr o Thm.cprop_of) CCas
-          |> fold_rev (Thm.forall_intr o Thm.global_cterm_of thy o Free) RIvs
+          |> fold_rev (Thm.forall_intr o Thm.cterm_of ctxt o Free) RIvs
 
         val P_recs = map mk_Prec RCs   (*  [P rec1, P rec2, ... ]  *)
 
@@ -645,7 +649,7 @@
           |> fold_rev (curry Logic.mk_implies) gs
           |> curry Logic.mk_implies (HOLogic.mk_Trueprop (D $ lhs))
           |> fold_rev mk_forall_rename (map fst oqs ~~ qs)
-          |> Thm.global_cterm_of thy
+          |> Thm.cterm_of ctxt
 
         val P_lhs = Thm.assume step
           |> fold Thm.forall_elim cqs
@@ -653,7 +657,7 @@
           |> fold Thm.elim_implies ags
           |> fold Thm.elim_implies P_recs
 
-        val res = Thm.global_cterm_of thy (HOLogic.mk_Trueprop (P $ x))
+        val res = Thm.cterm_of ctxt (HOLogic.mk_Trueprop (P $ x))
           |> Conv.arg_conv (Conv.arg_conv case_hyp_conv)
           |> Thm.symmetric (* P lhs == P x *)
           |> (fn eql => Thm.equal_elim eql P_lhs) (* "P x" *)
@@ -671,7 +675,7 @@
       |> fold (curry op COMP) cases (*  P x  *)
       |> Thm.implies_intr ihyp
       |> Thm.implies_intr (Thm.cprop_of x_D)
-      |> Thm.forall_intr (Thm.global_cterm_of thy x)
+      |> Thm.forall_intr (Thm.cterm_of ctxt x)
 
     val subset_induct_rule =
       acc_subset_induct
@@ -686,16 +690,15 @@
 
     val simple_induct_rule =
       subset_induct_rule
-      |> Thm.forall_intr (Thm.global_cterm_of thy D)
-      |> Thm.forall_elim (Thm.global_cterm_of thy acc_R)
+      |> Thm.forall_intr (Thm.cterm_of ctxt D)
+      |> Thm.forall_elim (Thm.cterm_of ctxt acc_R)
       |> atac 1 |> Seq.hd
       |> (curry op COMP) (acc_downward
-        |> (instantiate' [SOME (Thm.global_ctyp_of thy domT)]
-             (map (SOME o Thm.global_cterm_of thy) [R, x, z]))
-        |> Thm.forall_intr (Thm.global_cterm_of thy z)
-        |> Thm.forall_intr (Thm.global_cterm_of thy x))
-      |> Thm.forall_intr (Thm.global_cterm_of thy a)
-      |> Thm.forall_intr (Thm.global_cterm_of thy P)
+        |> (instantiate' [SOME (Thm.ctyp_of ctxt domT)] (map (SOME o Thm.cterm_of ctxt) [R, x, z]))
+        |> Thm.forall_intr (Thm.cterm_of ctxt z)
+        |> Thm.forall_intr (Thm.cterm_of ctxt x))
+      |> Thm.forall_intr (Thm.cterm_of ctxt a)
+      |> Thm.forall_intr (Thm.cterm_of ctxt P)
   in
     simple_induct_rule
   end
@@ -860,7 +863,7 @@
     val ((f, (_, f_defthm)), lthy) =
       PROFILE "def_fun" (define_function (defname ^ "_sumC_def") (fname, mixfix) domT ranT G default) lthy
 
-    val RCss = map (map (inst_RC (Proof_Context.theory_of lthy) fvar f)) RCss
+    val RCss = map (map (inst_RC lthy fvar f)) RCss
     val trees = map (Function_Context_Tree.inst_tree lthy fvar f) trees
 
     val ((R, RIntro_thmss, R_elim), lthy) =
@@ -906,7 +909,7 @@
           (mk_psimps newctxt globals R xclauses values f_iff) graph_is_function
 
         val simple_pinduct = PROFILE "Proving partial induction rule"
-          (mk_partial_induct_rule newthy globals R complete_thm) xclauses
+          (mk_partial_induct_rule newctxt globals R complete_thm) xclauses
 
         val total_intro = PROFILE "Proving nested termination rule"
           (mk_nest_term_rule newctxt globals R R_elim) xclauses

--- a/src/HOL/Tools/Function/function_elims.ML	Fri Mar 06 21:14:27 2015 +0100
+++ b/src/HOL/Tools/Function/function_elims.ML	Fri Mar 06 21:20:30 2015 +0100
@@ -79,8 +79,6 @@
 
 fun mk_partial_elim_rules ctxt result =
   let
-    val thy = Proof_Context.theory_of ctxt;
-
     val FunctionResult {fs, R, dom, psimps, cases, ...} = result;
     val n_fs = length fs;
 

--- a/src/HOL/Tools/Function/induction_schema.ML	Fri Mar 06 21:14:27 2015 +0100
+++ b/src/HOL/Tools/Function/induction_schema.ML	Fri Mar 06 21:20:30 2015 +0100
@@ -45,8 +45,8 @@
 fun sum_prod_conv ctxt = Raw_Simplifier.rewrite ctxt true
   (map meta (@{thm split_conv} :: @{thms sum.case}))
 
-fun term_conv thy cv t =
-  cv (Thm.global_cterm_of thy t)
+fun term_conv ctxt cv t =
+  cv (Thm.cterm_of ctxt t)
   |> Thm.prop_of |> Logic.dest_equals |> snd
 
 fun mk_relT T = HOLogic.mk_setT (HOLogic.mk_prodT (T, T))
@@ -194,7 +194,7 @@
       HOLogic.mk_Trueprop (list_comb (P, map Free xs))
       |> fold_rev (curry Logic.mk_implies) Cs
       |> fold_rev (Logic.all o Free) ws
-      |> term_conv thy (ind_atomize ctxt)
+      |> term_conv ctxt (ind_atomize ctxt)
       |> Object_Logic.drop_judgment thy
       |> HOLogic.tupled_lambda (foldr1 HOLogic.mk_prod (map Free xs))
   in

--- a/src/HOL/Tools/Function/pat_completeness.ML	Fri Mar 06 21:14:27 2015 +0100
+++ b/src/HOL/Tools/Function/pat_completeness.ML	Fri Mar 06 21:20:30 2015 +0100
@@ -23,10 +23,10 @@
 
 fun inst_free var inst = Thm.forall_elim inst o Thm.forall_intr var
 
-fun inst_case_thm thy x P thm =
+fun inst_case_thm ctxt x P thm =
   let val [Pv, xv] = Term.add_vars (Thm.prop_of thm) []
   in
-    thm |> cterm_instantiate (map (apply2 (Thm.global_cterm_of thy)) [(Var xv, x), (Var Pv, P)])
+    thm |> cterm_instantiate (map (apply2 (Thm.cterm_of ctxt)) [(Var xv, x), (Var Pv, P)])
   end
 
 fun invent_vars constr i =
@@ -40,26 +40,24 @@
    (avs, pvs, j)
  end
 
-fun filter_pats ctxt cons pvars [] = []
-  | filter_pats ctxt cons pvars (([], thm) :: pts) = raise Match
+fun filter_pats _ _ _ [] = []
+  | filter_pats _ _ _ (([], _) :: _) = raise Match
   | filter_pats ctxt cons pvars (((pat as Free _) :: pats, thm) :: pts) =
-    let val inst = list_comb (cons, pvars) in
-      (inst :: pats,
-        inst_free (Thm.cterm_of ctxt pat) (Thm.cterm_of ctxt inst) thm)
-        :: (filter_pats ctxt cons pvars pts)
-    end
-  | filter_pats thy cons pvars ((pat :: pats, thm) :: pts) =
-    if fst (strip_comb pat) = cons
-    then (pat :: pats, thm) :: (filter_pats thy cons pvars pts)
-    else filter_pats thy cons pvars pts
+      let val inst = list_comb (cons, pvars) in
+        (inst :: pats, inst_free (Thm.cterm_of ctxt pat) (Thm.cterm_of ctxt inst) thm) ::
+          filter_pats ctxt cons pvars pts
+      end
+  | filter_pats ctxt cons pvars ((pat :: pats, thm) :: pts) =
+      if fst (strip_comb pat) = cons
+      then (pat :: pats, thm) :: filter_pats ctxt cons pvars pts
+      else filter_pats ctxt cons pvars pts
 
 
-fun transform_pat _ avars c_assum ([] , thm) = raise Match
+fun transform_pat _ _ _ ([] , _) = raise Match
   | transform_pat ctxt avars c_assum (pat :: pats, thm) =
       let
         val (_, subps) = strip_comb pat
-        val eqs =
-          map (Thm.cterm_of ctxt o HOLogic.mk_Trueprop o HOLogic.mk_eq) (avars ~~ subps)
+        val eqs = map (Thm.cterm_of ctxt o HOLogic.mk_Trueprop o HOLogic.mk_eq) (avars ~~ subps)
         val c_eq_pat =
           simplify (put_simpset HOL_basic_ss ctxt addsimps (map Thm.assume eqs)) c_assum
       in
@@ -95,13 +93,12 @@
                   (Thm.cterm_of ctxt v) thm))) pts)
       else (* Cons case *)
         let
-          val thy = Proof_Context.theory_of ctxt
           val T as Type (tname, _) = fastype_of v
           val SOME {exhaust=case_thm, ...} = Ctr_Sugar.ctr_sugar_of ctxt tname
           val constrs = inst_constrs_of ctxt T
           val c_cases = map (constr_case ctxt P idx (v :: vs) pts) constrs
         in
-          inst_case_thm thy v P case_thm
+          inst_case_thm ctxt v P case_thm
           |> fold (curry op COMP) c_cases
         end
   | o_alg _ _ _ _ _ = raise Match

--- a/src/HOL/Tools/Function/relation.ML	Fri Mar 06 21:14:27 2015 +0100
+++ b/src/HOL/Tools/Function/relation.ML	Fri Mar 06 21:20:30 2015 +0100
@@ -15,17 +15,15 @@
 
 (* tactic version *)
 
-fun inst_state_tac inst st =
+fun inst_state_tac ctxt inst st =
   (case Term.add_vars (Thm.prop_of st) [] of  (* FIXME tactic should not inspect main conclusion *)
     [v as (_, T)] =>
-      let val thy = Thm.theory_of_thm st in
-        PRIMITIVE (Thm.instantiate ([], [(Thm.global_cterm_of thy (Var v), Thm.global_cterm_of thy (inst T))])) st
-      end
+      PRIMITIVE (Thm.instantiate ([], [(Thm.cterm_of ctxt (Var v), Thm.cterm_of ctxt (inst T))])) st
   | _ => Seq.empty);
 
 fun relation_tac ctxt rel i =
   TRY (Function_Common.termination_rule_tac ctxt i)
-  THEN inst_state_tac rel;
+  THEN inst_state_tac ctxt rel;
 
 
 (* version with type inference *)