optional proof context for unify operations, for the sake of proper local options;

--- a/src/Doc/Implementation/Tactic.thy	Sat Nov 08 17:39:01 2014 +0100
+++ b/src/Doc/Implementation/Tactic.thy	Sat Nov 08 21:31:51 2014 +0100
@@ -454,7 +454,7 @@
   \begin{mldecls}
   @{index_ML rotate_tac: "int -> int -> tactic"} \\
   @{index_ML distinct_subgoals_tac: tactic} \\
-  @{index_ML flexflex_tac: tactic} \\
+  @{index_ML flexflex_tac: "Proof.context -> tactic"} \\
   \end{mldecls}
 
   \begin{description}

--- a/src/HOL/Nominal/nominal_fresh_fun.ML	Sat Nov 08 17:39:01 2014 +0100
+++ b/src/HOL/Nominal/nominal_fresh_fun.ML	Sat Nov 08 21:31:51 2014 +0100
@@ -37,8 +37,8 @@
 val res_inst_tac_term' =
   gen_res_inst_tac_term (K Drule.cterm_instantiate) [];
 
-fun cut_inst_tac_term' tinst th =
-  res_inst_tac_term' tinst false (Rule_Insts.make_elim_preserve th);
+fun cut_inst_tac_term' ctxt tinst th =
+  res_inst_tac_term' tinst false (Rule_Insts.make_elim_preserve ctxt th);
 
 fun get_dyn_thm thy name atom_name =
   Global_Theory.get_thm thy name handle ERROR _ =>
@@ -76,7 +76,7 @@
    val x = hd (Misc_Legacy.term_vars (prop_of exists_fresh'));
  in
    fn st =>
-   (cut_inst_tac_term' [(x,s)] exists_fresh' 1 THEN
+   (cut_inst_tac_term' ctxt [(x,s)] exists_fresh' 1 THEN
    rtac fs_name_thm 1 THEN
    etac exE 1) st
   handle List.Empty  => all_tac st (* if we collected no variables then we do nothing *)

--- a/src/HOL/TLA/Intensional.thy	Sat Nov 08 17:39:01 2014 +0100
+++ b/src/HOL/TLA/Intensional.thy	Sat Nov 08 21:31:51 2014 +0100
@@ -262,7 +262,7 @@
   let
     (* analogous to RS, but using matching instead of resolution *)
     fun matchres tha i thb =
-      case Seq.chop 2 (Thm.biresolution true [(false,tha)] i thb) of
+      case Seq.chop 2 (Thm.biresolution NONE true [(false,tha)] i thb) of
           ([th],_) => th
         | ([],_)   => raise THM("matchres: no match", i, [tha,thb])
         |      _   => raise THM("matchres: multiple unifiers", i, [tha,thb])

--- a/src/HOL/Tools/Function/function_core.ML	Sat Nov 08 17:39:01 2014 +0100
+++ b/src/HOL/Tools/Function/function_core.ML	Sat Nov 08 21:31:51 2014 +0100
@@ -351,7 +351,8 @@
       map2 (mk_uniqueness_clause thy globals compat_store clausei) clauses rep_lemmas
 
     fun elim_implies_eta A AB =
-      Thm.bicompose {flatten = false, match = true, incremented = false} (false, A, 0) 1 AB
+      Thm.bicompose (SOME ctxt) {flatten = false, match = true, incremented = false}
+        (false, A, 0) 1 AB
       |> Seq.list_of |> the_single
 
     val uniqueness = G_cases

--- a/src/HOL/Tools/Function/induction_schema.ML	Sat Nov 08 17:39:01 2014 +0100
+++ b/src/HOL/Tools/Function/induction_schema.ML	Sat Nov 08 21:31:51 2014 +0100
@@ -387,7 +387,7 @@
     val nbranches = length branches
     val npres = length pres
   in
-    Thm.bicompose {flatten = false, match = false, incremented = false}
+    Thm.bicompose (SOME ctxt') {flatten = false, match = false, incremented = false}
       (false, res, length newgoals) i
     THEN term_tac (i + nbranches + npres)
     THEN (EVERY (map (TRY o pres_tac) ((i + nbranches + npres - 1) downto (i + nbranches))))

--- a/src/HOL/Tools/Metis/metis_reconstruct.ML	Sat Nov 08 17:39:01 2014 +0100
+++ b/src/HOL/Tools/Metis/metis_reconstruct.ML	Sat Nov 08 21:31:51 2014 +0100
@@ -187,7 +187,7 @@
   let
     val tha = incr_type_indexes (1 + Thm.maxidx_of thb) tha
     fun res (tha, thb) =
-      (case Thm.bicompose {flatten = true, match = false, incremented = true}
+      (case Thm.bicompose (SOME ctxt) {flatten = true, match = false, incremented = true}
             (false, tha, nprems_of tha) i thb
            |> Seq.list_of |> distinct Thm.eq_thm of
         [th] => th
@@ -211,7 +211,7 @@
           |> AList.group (op =)
           |> maps (fn ((s, _), T :: Ts) => map (fn T' => (Free (s, T), Free (s, T'))) Ts)
           |> rpair (Envir.empty ~1)
-          |-> fold (Pattern.unify thy)
+          |-> fold (Pattern.unify (Context.Proof ctxt))
           |> Envir.type_env |> Vartab.dest
           |> map (fn (x, (S, T)) => pairself (ctyp_of thy) (TVar (x, S), T))
       in
@@ -747,7 +747,7 @@
               THEN rotate_tac (rotation_of_subgoal i) i
               THEN PRIMITIVE (unify_first_prem_with_concl thy i)
               THEN assume_tac i
-              THEN flexflex_tac)))
+              THEN flexflex_tac ctxt')))
       handle ERROR msg =>
         cat_error msg
           "Cannot replay Metis proof in Isabelle: error when discharging Skolem assumptions"

--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_specialisation.ML	Sat Nov 08 17:39:01 2014 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_specialisation.ML	Sat Nov 08 21:31:51 2014 +0100
@@ -83,7 +83,7 @@
     fun specialise_intro intro =
       (let
         val (prems, concl) = Logic.strip_horn (prop_of intro)
-        val env = Pattern.unify thy
+        val env = Pattern.unify (Context.Theory thy)
           (HOLogic.mk_Trueprop (list_comb (pred, pats)), concl) (Envir.empty 0)
         val prems = map (Envir.norm_term env) prems
         val args = map (Envir.norm_term env) result_pats

--- a/src/HOL/Tools/Quotient/quotient_tacs.ML	Sat Nov 08 17:39:01 2014 +0100
+++ b/src/HOL/Tools/Quotient/quotient_tacs.ML	Sat Nov 08 21:31:51 2014 +0100
@@ -80,7 +80,7 @@
 
 fun get_match_inst thy pat trm =
   let
-    val univ = Unify.matchers thy [(pat, trm)]
+    val univ = Unify.matchers (Context.Theory thy) [(pat, trm)]
     val SOME (env, _) = Seq.pull univ           (* raises Bind, if no unifier *) (* FIXME fragile *)
     val tenv = Vartab.dest (Envir.term_env env)
     val tyenv = Vartab.dest (Envir.type_env env)

--- a/src/HOL/Tools/TFL/casesplit.ML	Sat Nov 08 17:39:01 2014 +0100
+++ b/src/HOL/Tools/TFL/casesplit.ML	Sat Nov 08 21:31:51 2014 +0100
@@ -122,7 +122,7 @@
       (* check if we are a member of splitths - FIXME: quicker and
       more flexible with discrim net. *)
       fun solve_by_splitth th split =
-        Thm.biresolution false [(false,split)] 1 th;
+        Thm.biresolution (SOME ctxt) false [(false,split)] 1 th;
 
       fun split th =
         (case find_thms_split splitths 1 th of

--- a/src/Provers/blast.ML	Sat Nov 08 17:39:01 2014 +0100
+++ b/src/Provers/blast.ML	Sat Nov 08 21:31:51 2014 +0100
@@ -461,7 +461,7 @@
 
 
 (*Like dup_elim, but puts the duplicated major premise FIRST*)
-fun rev_dup_elim th = (th RSN (2, revcut_rl)) |> Thm.assumption 2 |> Seq.hd;
+fun rev_dup_elim th = (th RSN (2, revcut_rl)) |> Thm.assumption NONE 2 |> Seq.hd;
 
 
 (*Rotate the assumptions in all new subgoals for the LIFO discipline*)

--- a/src/Provers/classical.ML	Sat Nov 08 17:39:01 2014 +0100
+++ b/src/Provers/classical.ML	Sat Nov 08 21:31:51 2014 +0100
@@ -207,7 +207,7 @@
 
 fun dup_elim th =  (* FIXME proper context!? *)
   let
-    val rl = (th RSN (2, revcut_rl)) |> Thm.assumption 2 |> Seq.hd;
+    val rl = (th RSN (2, revcut_rl)) |> Thm.assumption NONE 2 |> Seq.hd;
     val ctxt = Proof_Context.init_global (Thm.theory_of_thm rl);
   in rule_by_tactic ctxt (TRYALL (eresolve_tac [revcut_rl])) rl end;
 
@@ -906,7 +906,7 @@
     val {xtra_netpair, ...} = rep_claset_of ctxt;
     val rules3 = Context_Rules.find_rules_netpair true facts goal xtra_netpair;
     val rules = rules1 @ rules2 @ rules3 @ rules4;
-    val ruleq = Drule.multi_resolves facts rules;
+    val ruleq = Drule.multi_resolves (SOME ctxt) facts rules;
     val _ = Method.trace ctxt rules;
   in
     fn st => Seq.maps (fn rule => resolve_tac [rule] i st) ruleq

--- a/src/Provers/hypsubst.ML	Sat Nov 08 17:39:01 2014 +0100
+++ b/src/Provers/hypsubst.ML	Sat Nov 08 21:31:51 2014 +0100
@@ -196,7 +196,7 @@
 
 val imp_intr_tac = resolve_tac [Data.imp_intr];
 
-fun rev_dup_elim th = (th RSN (2, revcut_rl)) |> Thm.assumption 2 |> Seq.hd;
+fun rev_dup_elim th = (th RSN (2, revcut_rl)) |> Thm.assumption NONE 2 |> Seq.hd;
 val dup_subst = rev_dup_elim ssubst
 
 (* FIXME: "etac Data.rev_mp i" will not behave as expected if goal has *)

--- a/src/Pure/Isar/calculation.ML	Sat Nov 08 17:39:01 2014 +0100
+++ b/src/Pure/Isar/calculation.ML	Sat Nov 08 21:31:51 2014 +0100
@@ -85,8 +85,9 @@
 
 (* symmetric *)
 
-val symmetric = Thm.rule_attribute (fn x => fn th =>
-  (case Seq.chop 2 (Drule.multi_resolves [th] (#2 (#1 (Data.get x)))) of
+val symmetric = Thm.rule_attribute (fn context => fn th =>
+  (case Seq.chop 2
+      (Drule.multi_resolves (SOME (Context.proof_of context)) [th] (#2 (#1 (Data.get context)))) of
     ([th'], _) => Drule.zero_var_indexes th'
   | ([], _) => raise THM ("symmetric: no unifiers", 1, [th])
   | _ => raise THM ("symmetric: multiple unifiers", 1, [th])));
@@ -155,7 +156,7 @@
             (case ths of
               [] => Item_Net.content (#1 (get_rules ctxt))
             | th :: _ => Item_Net.retrieve (#1 (get_rules ctxt)) (strip_assums_concl th)))
-        |> Seq.of_list |> Seq.maps (Drule.multi_resolve ths)
+        |> Seq.of_list |> Seq.maps (Drule.multi_resolve (SOME ctxt) ths)
         |> Seq.map (check_projection ths))
         (Seq.single (Seq.Error (fn () =>
           (Pretty.string_of o Pretty.block o Pretty.fbreaks)

--- a/src/Pure/Isar/method.ML	Sat Nov 08 17:39:01 2014 +0100
+++ b/src/Pure/Isar/method.ML	Sat Nov 08 21:31:51 2014 +0100
@@ -185,7 +185,7 @@
     | _ => K no_tac));
 
 fun finish immed ctxt =
-  METHOD (K ((if immed then all_assm_tac ctxt else all_tac) THEN flexflex_tac));
+  METHOD (K ((if immed then all_assm_tac ctxt else all_tac) THEN flexflex_tac ctxt));
 
 end;
 
@@ -205,7 +205,9 @@
 fun gen_rule_tac tac ctxt rules facts =
   (fn i => fn st =>
     if null facts then tac rules i st
-    else Seq.maps (fn rule => (tac o single) rule i st) (Drule.multi_resolves facts rules))
+    else
+      Seq.maps (fn rule => (tac o single) rule i st)
+        (Drule.multi_resolves (SOME ctxt) facts rules))
   THEN_ALL_NEW Goal.norm_hhf_tac ctxt;
 
 fun gen_arule_tac tac ctxt j rules facts =

--- a/src/Pure/Isar/proof.ML	Sat Nov 08 17:39:01 2014 +0100
+++ b/src/Pure/Isar/proof.ML	Sat Nov 08 21:31:51 2014 +0100
@@ -471,7 +471,7 @@
     val th =
       (Goal.conclude (if length (flat propss) > 1 then Thm.norm_proof goal else goal)
         handle THM _ => lost_structure ())
-      |> Drule.flexflex_unique
+      |> Drule.flexflex_unique (SOME ctxt)
       |> Thm.check_shyps (Variable.sorts_of ctxt)
       |> Thm.check_hyps (Context.Proof ctxt);
 
@@ -480,8 +480,9 @@
       Conjunction.elim_balanced (length goal_propss) th
       |> map2 Conjunction.elim_balanced (map length goal_propss)
       handle THM _ => lost_structure ();
-    val _ = Unify.matches_list thy (flat goal_propss) (map Thm.prop_of (flat results)) orelse
-      error ("Proved a different theorem:\n" ^ Display.string_of_thm ctxt th);
+    val _ =
+      Unify.matches_list (Context.Proof ctxt) (flat goal_propss) (map Thm.prop_of (flat results))
+        orelse error ("Proved a different theorem:\n" ^ Display.string_of_thm ctxt th);
 
     fun recover_result ([] :: pss) thss = [] :: recover_result pss thss
       | recover_result (_ :: pss) (ths :: thss) = ths :: recover_result pss thss

--- a/src/Pure/Isar/proof_context.ML	Sat Nov 08 17:39:01 2014 +0100
+++ b/src/Pure/Isar/proof_context.ML	Sat Nov 08 21:31:51 2014 +0100
@@ -790,7 +790,7 @@
 (* simult_matches *)
 
 fun simult_matches ctxt (t, pats) =
-  (case Seq.pull (Unify.matchers (theory_of ctxt) (map (rpair t) pats)) of
+  (case Seq.pull (Unify.matchers (Context.Proof ctxt) (map (rpair t) pats)) of
     NONE => error "Pattern match failed!"
   | SOME (env, _) => Vartab.fold (fn (v, (_, t)) => cons (v, t)) (Envir.term_env env) []);
 
@@ -898,17 +898,18 @@
 
 local
 
-fun comp_hhf_tac th i st =
-  PRIMSEQ (Thm.bicompose {flatten = true, match = false, incremented = true}
+fun comp_hhf_tac ctxt th i st =
+  PRIMSEQ (Thm.bicompose (SOME ctxt) {flatten = true, match = false, incremented = true}
     (false, Drule.lift_all (Thm.cprem_of st i) th, 0) i) st;
 
-fun comp_incr_tac [] _ = no_tac
-  | comp_incr_tac (th :: ths) i =
-      (fn st => comp_hhf_tac (Drule.incr_indexes st th) i st) APPEND comp_incr_tac ths i;
+fun comp_incr_tac _ [] _ = no_tac
+  | comp_incr_tac ctxt (th :: ths) i =
+      (fn st => comp_hhf_tac ctxt (Drule.incr_indexes st th) i st) APPEND
+      comp_incr_tac ctxt ths i;
 
 in
 
-fun fact_tac ctxt facts = Goal.norm_hhf_tac ctxt THEN' comp_incr_tac facts;
+fun fact_tac ctxt facts = Goal.norm_hhf_tac ctxt THEN' comp_incr_tac ctxt facts;
 
 fun potential_facts ctxt prop =
   Facts.could_unify (facts_of ctxt) (Term.strip_all_body prop);

--- a/src/Pure/Isar/rule_cases.ML	Sat Nov 08 17:39:01 2014 +0100
+++ b/src/Pure/Isar/rule_cases.ML	Sat Nov 08 21:31:51 2014 +0100
@@ -221,7 +221,7 @@
     th
     |> unfold_prems ctxt n defs
     |> unfold_prems_concls ctxt defs
-    |> Drule.multi_resolve (take m facts)
+    |> Drule.multi_resolve (SOME ctxt) (take m facts)
     |> Seq.map (pair (xx, (n - m, drop m facts)))
   end;
 

--- a/src/Pure/Proof/extraction.ML	Sat Nov 08 17:39:01 2014 +0100
+++ b/src/Pure/Proof/extraction.ML	Sat Nov 08 21:31:51 2014 +0100
@@ -107,7 +107,7 @@
           val env' = Envir.Envir
             {maxidx = fold (fn (t, u) => Term.maxidx_term t #> Term.maxidx_term u) prems' ~1,
              tenv = tenv, tyenv = Tenv};
-          val env'' = fold (Pattern.unify thy o pairself (lookup rew)) prems' env';
+          val env'' = fold (Pattern.unify (Context.Theory thy) o pairself (lookup rew)) prems' env';
         in SOME (Envir.norm_term env'' (inc (ren tm2)))
         end handle Pattern.MATCH => NONE | Pattern.Unif => NONE)
           (sort (int_ord o pairself fst)

--- a/src/Pure/Proof/reconstruct.ML	Sat Nov 08 17:39:01 2014 +0100
+++ b/src/Pure/Proof/reconstruct.ML	Sat Nov 08 21:31:51 2014 +0100
@@ -121,7 +121,7 @@
         val t' = mk_abs Ts t;
         val u' = mk_abs Ts u
       in
-        (prop, prf, cs, Pattern.unify thy (t', u') env, vTs)
+        (prop, prf, cs, Pattern.unify (Context.Theory thy) (t', u') env, vTs)
         handle Pattern.Pattern =>
             let val (cs', env') = decompose thy [] (t', u') env
             in (prop, prf, cs @ cs', env', vTs) end
@@ -263,7 +263,7 @@
                   val tn2 = Envir.norm_term bigenv t2
                 in
                   if Pattern.pattern tn1 andalso Pattern.pattern tn2 then
-                    (Pattern.unify thy (tn1, tn2) env, ps) handle Pattern.Unif =>
+                    (Pattern.unify (Context.Theory thy) (tn1, tn2) env, ps) handle Pattern.Unif =>
                        cantunify thy (tn1, tn2)
                   else
                     let val (cs', env') = decompose thy [] (tn1, tn2) env

--- a/src/Pure/Tools/rule_insts.ML	Sat Nov 08 17:39:01 2014 +0100
+++ b/src/Pure/Tools/rule_insts.ML	Sat Nov 08 21:31:51 2014 +0100
@@ -24,7 +24,7 @@
     (binding * string option * mixfix) list -> thm -> thm
   val read_instantiate: Proof.context -> (indexname * string) list -> string list -> thm -> thm
   val instantiate_tac: Proof.context -> (indexname * string) list -> string list -> tactic
-  val make_elim_preserve: thm -> thm
+  val make_elim_preserve: Proof.context -> thm -> thm
   val method: (Proof.context -> (indexname * string) list -> thm -> int -> tactic) ->
     (Proof.context -> thm list -> int -> tactic) -> (Proof.context -> Proof.method) context_parser
 end;
@@ -280,7 +280,7 @@
 
 (* forward resolution *)
 
-fun make_elim_preserve rl =
+fun make_elim_preserve ctxt rl =
   let
     val cert = Thm.cterm_of (Thm.theory_of_thm rl);
     val maxidx = Thm.maxidx_of rl;
@@ -290,7 +290,7 @@
         (cvar ("W", 0), cvar ("W", maxidx + 1))]) Drule.revcut_rl;
   in
     (case Seq.list_of
-      (Thm.bicompose {flatten = true, match = false, incremented = false}
+      (Thm.bicompose (SOME ctxt) {flatten = true, match = false, incremented = false}
         (false, rl, Thm.nprems_of rl) 1 revcut_rl')
      of
       [th] => th
@@ -298,13 +298,13 @@
   end;
 
 (*instantiate and cut -- for atomic fact*)
-fun cut_inst_tac ctxt insts rule = res_inst_tac ctxt insts (make_elim_preserve rule);
+fun cut_inst_tac ctxt insts rule = res_inst_tac ctxt insts (make_elim_preserve ctxt rule);
 
 (*forward tactic applies a rule to an assumption without deleting it*)
 fun forw_inst_tac ctxt insts rule = cut_inst_tac ctxt insts rule THEN' assume_tac;
 
 (*dresolve tactic applies a rule to replace an assumption*)
-fun dres_inst_tac ctxt insts rule = eres_inst_tac ctxt insts (make_elim_preserve rule);
+fun dres_inst_tac ctxt insts rule = eres_inst_tac ctxt insts (make_elim_preserve ctxt rule);
 
 
 (* derived tactics *)

--- a/src/Pure/drule.ML	Sat Nov 08 17:39:01 2014 +0100
+++ b/src/Pure/drule.ML	Sat Nov 08 21:31:51 2014 +0100
@@ -59,15 +59,15 @@
   val strip_type: ctyp -> ctyp list * ctyp
   val beta_conv: cterm -> cterm -> cterm
   val types_sorts: thm -> (indexname-> typ option) * (indexname-> sort option)
-  val flexflex_unique: thm -> thm
+  val flexflex_unique: Proof.context option -> thm -> thm
   val export_without_context: thm -> thm
   val export_without_context_open: thm -> thm
   val store_thm: binding -> thm -> thm
   val store_standard_thm: binding -> thm -> thm
   val store_thm_open: binding -> thm -> thm
   val store_standard_thm_open: binding -> thm -> thm
-  val multi_resolve: thm list -> thm -> thm Seq.seq
-  val multi_resolves: thm list -> thm list -> thm Seq.seq
+  val multi_resolve: Proof.context option -> thm list -> thm -> thm Seq.seq
+  val multi_resolves: Proof.context option -> thm list -> thm list -> thm Seq.seq
   val compose: thm * int * thm -> thm
   val equals_cong: thm
   val imp_cong: thm
@@ -268,9 +268,9 @@
 
 (*Squash a theorem's flexflex constraints provided it can be done uniquely.
   This step can lose information.*)
-fun flexflex_unique th =
+fun flexflex_unique opt_ctxt th =
   if null (Thm.tpairs_of th) then th else
-    case distinct Thm.eq_thm (Seq.list_of (Thm.flexflex_rule th)) of
+    case distinct Thm.eq_thm (Seq.list_of (Thm.flexflex_rule opt_ctxt th)) of
       [th] => th
     | []   => raise THM("flexflex_unique: impossible constraints", 0, [th])
     |  _   => raise THM("flexflex_unique: multiple unifiers", 0, [th]);
@@ -289,7 +289,7 @@
     #> Thm.varifyT_global);
 
 val export_without_context =
-  flexflex_unique
+  flexflex_unique NONE
   #> export_without_context_open
   #> Thm.close_derivation;
 
@@ -315,19 +315,21 @@
 
 (*Resolution: multiple arguments, multiple results*)
 local
-  fun res th i rule =
-    Thm.biresolution false [(false, th)] i rule handle THM _ => Seq.empty;
+  fun res opt_ctxt th i rule =
+    Thm.biresolution opt_ctxt false [(false, th)] i rule handle THM _ => Seq.empty;
 
-  fun multi_res _ [] rule = Seq.single rule
-    | multi_res i (th :: ths) rule = Seq.maps (res th i) (multi_res (i + 1) ths rule);
+  fun multi_res _ _ [] rule = Seq.single rule
+    | multi_res opt_ctxt i (th :: ths) rule =
+        Seq.maps (res opt_ctxt th i) (multi_res opt_ctxt (i + 1) ths rule);
 in
-  val multi_resolve = multi_res 1;
-  fun multi_resolves facts rules = Seq.maps (multi_resolve facts) (Seq.of_list rules);
+  fun multi_resolve opt_ctxt = multi_res opt_ctxt 1;
+  fun multi_resolves opt_ctxt facts rules =
+    Seq.maps (multi_resolve opt_ctxt facts) (Seq.of_list rules);
 end;
 
 (*Resolution: exactly one resolvent must be produced*)
 fun tha RSN (i, thb) =
-  (case Seq.chop 2 (Thm.biresolution false [(false, tha)] i thb) of
+  (case Seq.chop 2 (Thm.biresolution NONE false [(false, tha)] i thb) of
     ([th], _) => th
   | ([], _) => raise THM ("RSN: no unifiers", i, [tha, thb])
   | _ => raise THM ("RSN: multiple unifiers", i, [tha, thb]));
@@ -337,7 +339,7 @@
 
 (*For joining lists of rules*)
 fun thas RLN (i, thbs) =
-  let val resolve = Thm.biresolution false (map (pair false) thas) i
+  let val resolve = Thm.biresolution NONE false (map (pair false) thas) i
       fun resb thb = Seq.list_of (resolve thb) handle THM _ => []
   in maps resb thbs end;
 
@@ -345,7 +347,7 @@
 
 (*Isar-style multi-resolution*)
 fun bottom_rl OF rls =
-  (case Seq.chop 2 (multi_resolve rls bottom_rl) of
+  (case Seq.chop 2 (multi_resolve NONE rls bottom_rl) of
     ([th], _) => th
   | ([], _) => raise THM ("OF: no unifiers", 0, bottom_rl :: rls)
   | _ => raise THM ("OF: multiple unifiers", 0, bottom_rl :: rls));
@@ -358,7 +360,7 @@
   with no lifting or renaming!  Q may contain ==> or meta-quants
   ALWAYS deletes premise i *)
 fun compose (tha, i, thb) =
-  Thm.bicompose {flatten = true, match = false, incremented = false} (false, tha, 0) i thb
+  Thm.bicompose NONE {flatten = true, match = false, incremented = false} (false, tha, 0) i thb
   |> Seq.list_of |> distinct Thm.eq_thm
   |> (fn [th] => th | _ => raise THM ("compose: unique result expected", i, [tha, thb]));
 
@@ -739,7 +741,7 @@
 
 (*compose Q and [Q1,Q2,...,Qk]==>R to [Q2,...,Qk]==>R getting unique result*)
 fun comp incremented th1 th2 =
-  Thm.bicompose {flatten = true, match = false, incremented = incremented} (false, th1, 0) 1 th2
+  Thm.bicompose NONE {flatten = true, match = false, incremented = incremented} (false, th1, 0) 1 th2
   |> Seq.list_of |> distinct Thm.eq_thm
   |> (fn [th] => th | _ => raise THM ("COMP", 1, [th1, th2]));
 
@@ -753,7 +755,7 @@
 
 fun comp_no_flatten (th, n) i rule =
   (case distinct Thm.eq_thm (Seq.list_of
-      (Thm.bicompose {flatten = false, match = false, incremented = true}
+      (Thm.bicompose NONE {flatten = false, match = false, incremented = true}
         (false, th, n) i (incr_indexes th rule))) of
     [th'] => th'
   | [] => raise THM ("comp_no_flatten", i, [th, rule])

--- a/src/Pure/goal.ML	Sat Nov 08 17:39:01 2014 +0100
+++ b/src/Pure/goal.ML	Sat Nov 08 21:31:51 2014 +0100
@@ -97,7 +97,7 @@
 (* normal form *)
 
 fun norm_result ctxt =
-  Drule.flexflex_unique
+  Drule.flexflex_unique (SOME ctxt)
   #> Raw_Simplifier.norm_hhf_protect ctxt
   #> Thm.strip_shyps
   #> Drule.zero_var_indexes;
@@ -144,7 +144,7 @@
       cert (Logic.varify_types_global (fold_rev Logic.all xs (Logic.list_implies (As, prop))))
       |> Thm.weaken_sorts (Variable.sorts_of ctxt);
     val global_result = result |> Future.map
-      (Drule.flexflex_unique #>
+      (Drule.flexflex_unique (SOME ctxt) #>
         Thm.adjust_maxidx_thm ~1 #>
         Drule.implies_intr_list assms #>
         Drule.forall_intr_list fixes #>
@@ -216,12 +216,13 @@
               Theory.subthy (theory_of_thm st, thy) orelse err "Bad background theory of goal state";
             val res =
               (finish ctxt' st
-                |> Drule.flexflex_unique
+                |> Drule.flexflex_unique (SOME ctxt')
                 |> Thm.check_shyps sorts
                 |> Thm.check_hyps (Context.Proof ctxt'))
               handle THM (msg, _, _) => err msg | ERROR msg => err msg;
           in
-            if Unify.matches_list thy [Thm.term_of stmt] [Thm.prop_of res] then res
+            if Unify.matches_list (Context.Proof ctxt') [Thm.term_of stmt] [Thm.prop_of res]
+            then res
             else err ("Proved a different theorem: " ^ Syntax.string_of_term ctxt' (Thm.prop_of res))
           end);
     val res =

--- a/src/Pure/par_tactical.ML	Sat Nov 08 17:39:01 2014 +0100
+++ b/src/Pure/par_tactical.ML	Sat Nov 08 21:31:51 2014 +0100
@@ -35,7 +35,7 @@
 
 fun retrofit st' =
   rotate_prems ~1 #>
-  Thm.bicompose {flatten = false, match = false, incremented = false}
+  Thm.bicompose NONE {flatten = false, match = false, incremented = false}
       (false, Goal.conclude st', Thm.nprems_of st') 1;
 
 in

--- a/src/Pure/pattern.ML	Sat Nov 08 17:39:01 2014 +0100
+++ b/src/Pure/pattern.ML	Sat Nov 08 21:31:51 2014 +0100
@@ -12,8 +12,13 @@
 
 signature PATTERN =
 sig
+  exception Unif
+  exception Pattern
   val unify_trace_failure_raw: Config.raw
   val unify_trace_failure: bool Config.T
+  val unify_types: Context.generic -> typ * typ -> Envir.env -> Envir.env
+  val unify: Context.generic -> term * term -> Envir.env -> Envir.env
+  exception MATCH
   val match: theory -> term * term -> Type.tyenv * Envir.tenv -> Type.tyenv * Envir.tenv
   val first_order_match: theory -> term * term
     -> Type.tyenv * Envir.tenv -> Type.tyenv * Envir.tenv
@@ -21,16 +26,11 @@
   val matchess: theory -> term list * term list -> bool
   val equiv: theory -> term * term -> bool
   val matches_subterm: theory -> term * term -> bool
-  val unify_types: theory -> typ * typ -> Envir.env -> Envir.env
-  val unify: theory -> term * term -> Envir.env -> Envir.env
   val first_order: term -> bool
   val pattern: term -> bool
   val match_rew: theory -> term -> term * term -> (term * term) option
   val rewrite_term: theory -> (term * term) list -> (term -> term option) list -> term -> term
   val rewrite_term_top: theory -> (term * term) list -> (term -> term option) list -> term -> term
-  exception Unif
-  exception MATCH
-  exception Pattern
 end;
 
 structure Pattern: PATTERN =
@@ -40,59 +40,62 @@
 exception Pattern;
 
 val unify_trace_failure_raw =
-  Config.declare_global ("unify_trace_failure", @{here}) (fn _ => Config.Bool false);
+  Config.declare ("unify_trace_failure", @{here}) (fn _ => Config.Bool false);
 val unify_trace_failure = Config.bool unify_trace_failure_raw;
 
-fun string_of_term thy env binders t =
-  Syntax.string_of_term_global thy
-    (Envir.norm_term env (subst_bounds (map Free binders, t)));
+fun string_of_term ctxt env binders t =
+  Syntax.string_of_term ctxt (Envir.norm_term env (subst_bounds (map Free binders, t)));
 
 fun bname binders i = fst (nth binders i);
 fun bnames binders is = space_implode " " (map (bname binders) is);
 
-fun typ_clash thy (tye,T,U) =
-  if Config.get_global thy unify_trace_failure
-  then let val t = Syntax.string_of_typ_global thy (Envir.norm_type tye T)
-           and u = Syntax.string_of_typ_global thy (Envir.norm_type tye U)
-       in tracing("The following types do not unify:\n" ^ t ^ "\n" ^ u) end
-  else ()
+fun typ_clash context (tye,T,U) =
+  if Config.get_generic context unify_trace_failure then
+    let
+      val ctxt = Context.proof_of context;
+      val t = Syntax.string_of_typ ctxt (Envir.norm_type tye T);
+      val u = Syntax.string_of_typ ctxt (Envir.norm_type tye U);
+    in tracing ("The following types do not unify:\n" ^ t ^ "\n" ^ u) end
+  else ();
 
-fun clash thy a b =
-  if Config.get_global thy unify_trace_failure then tracing("Clash: " ^ a ^ " =/= " ^ b) else ()
+fun clash context a b =
+  if Config.get_generic context unify_trace_failure
+  then tracing ("Clash: " ^ a ^ " =/= " ^ b) else ();
 
 fun boundVar binders i =
   "bound variable " ^ bname binders i ^ " (depth " ^ string_of_int i ^ ")";
 
-fun clashBB thy binders i j =
-  if Config.get_global thy unify_trace_failure
-  then clash thy (boundVar binders i) (boundVar binders j)
-  else ()
+fun clashBB context binders i j =
+  if Config.get_generic context unify_trace_failure
+  then clash context (boundVar binders i) (boundVar binders j) else ();
 
-fun clashB thy binders i s =
-  if Config.get_global thy unify_trace_failure
-  then clash thy (boundVar binders i) s
-  else ()
+fun clashB context binders i s =
+  if Config.get_generic context unify_trace_failure
+  then clash context (boundVar binders i) s else ();
 
-fun proj_fail thy (env,binders,F,_,is,t) =
-  if Config.get_global thy unify_trace_failure
-  then let val f = Term.string_of_vname F
-           val xs = bnames binders is
-           val u = string_of_term thy env binders t
-           val ys = bnames binders (subtract (op =) is (loose_bnos t))
-       in tracing("Cannot unify variable " ^ f ^
-               " (depending on bound variables " ^ xs ^ ")\nwith term " ^ u ^
-               "\nTerm contains additional bound variable(s) " ^ ys)
-       end
-  else ()
+fun proj_fail context (env,binders,F,_,is,t) =
+  if Config.get_generic context unify_trace_failure then
+    let
+      val ctxt = Context.proof_of context
+      val f = Term.string_of_vname F
+      val xs = bnames binders is
+      val u = string_of_term ctxt env binders t
+      val ys = bnames binders (subtract (op =) is (loose_bnos t))
+    in
+      tracing ("Cannot unify variable " ^ f ^
+        " (depending on bound variables " ^ xs ^ ")\nwith term " ^ u ^
+        "\nTerm contains additional bound variable(s) " ^ ys)
+    end
+  else ();
 
-fun ocheck_fail thy (F,t,binders,env) =
-  if Config.get_global thy unify_trace_failure
-  then let val f = Term.string_of_vname F
-           val u = string_of_term thy env binders t
-       in tracing("Variable " ^ f ^ " occurs in term\n" ^ u ^
-                  "\nCannot unify!\n")
-       end
-  else ()
+fun ocheck_fail context (F,t,binders,env) =
+  if Config.get_generic context unify_trace_failure then
+    let
+      val ctxt = Context.proof_of context
+      val f = Term.string_of_vname F
+      val u = string_of_term ctxt env binders t
+    in tracing ("Variable " ^ f ^ " occurs in term\n" ^ u ^ "\nCannot unify!\n") end
+  else ();
 
 fun occurs(F,t,env) =
     let fun occ(Var (G, T))   = (case Envir.lookup env (G, T) of
@@ -230,55 +233,57 @@
                  end;
   in if Term_Ord.indexname_ord (G,F) = LESS then ff(F,Fty,is,G,Gty,js) else ff(G,Gty,js,F,Fty,is) end
 
-fun unify_types thy (T, U) (env as Envir.Envir {maxidx, tenv, tyenv}) =
+fun unify_types context (T, U) (env as Envir.Envir {maxidx, tenv, tyenv}) =
   if T = U then env
   else
-    let val (tyenv', maxidx') = Sign.typ_unify thy (U, T) (tyenv, maxidx)
+    let
+      val thy = Context.theory_of context
+      val (tyenv', maxidx') = Sign.typ_unify thy (U, T) (tyenv, maxidx)
     in Envir.Envir {maxidx = maxidx', tenv = tenv, tyenv = tyenv'} end
-    handle Type.TUNIFY => (typ_clash thy (tyenv, T, U); raise Unif);
+    handle Type.TUNIFY => (typ_clash context (tyenv, T, U); raise Unif);
 
-fun unif thy binders (s,t) env = case (Envir.head_norm env s, Envir.head_norm env t) of
+fun unif context binders (s,t) env = case (Envir.head_norm env s, Envir.head_norm env t) of
       (Abs(ns,Ts,ts),Abs(nt,Tt,tt)) =>
          let val name = if ns = "" then nt else ns
-         in unif thy ((name,Ts)::binders) (ts,tt) (unify_types thy (Ts, Tt) env) end
-    | (Abs(ns,Ts,ts),t) => unif thy ((ns,Ts)::binders) (ts,(incr t)$Bound(0)) env
-    | (t,Abs(nt,Tt,tt)) => unif thy ((nt,Tt)::binders) ((incr t)$Bound(0),tt) env
-    | p => cases thy (binders,env,p)
+         in unif context ((name,Ts)::binders) (ts,tt) (unify_types context (Ts, Tt) env) end
+    | (Abs(ns,Ts,ts),t) => unif context ((ns,Ts)::binders) (ts,(incr t)$Bound(0)) env
+    | (t,Abs(nt,Tt,tt)) => unif context ((nt,Tt)::binders) ((incr t)$Bound(0),tt) env
+    | p => cases context (binders,env,p)
 
-and cases thy (binders,env,(s,t)) = case (strip_comb s,strip_comb t) of
+and cases context (binders,env,(s,t)) = case (strip_comb s,strip_comb t) of
        ((Var(F,Fty),ss),(Var(G,Gty),ts)) =>
          if F = G then flexflex1(env,binders,F,Fty,ints_of' env ss,ints_of' env ts)
                   else flexflex2(env,binders,F,Fty,ints_of' env ss,G,Gty,ints_of' env ts)
-      | ((Var(F,Fty),ss),_)           => flexrigid thy (env,binders,F,Fty,ints_of' env ss,t)
-      | (_,(Var(F,Fty),ts))           => flexrigid thy (env,binders,F,Fty,ints_of' env ts,s)
-      | ((Const c,ss),(Const d,ts))   => rigidrigid thy (env,binders,c,d,ss,ts)
-      | ((Free(f),ss),(Free(g),ts))   => rigidrigid thy (env,binders,f,g,ss,ts)
-      | ((Bound(i),ss),(Bound(j),ts)) => rigidrigidB thy (env,binders,i,j,ss,ts)
+      | ((Var(F,Fty),ss),_)           => flexrigid context (env,binders,F,Fty,ints_of' env ss,t)
+      | (_,(Var(F,Fty),ts))           => flexrigid context (env,binders,F,Fty,ints_of' env ts,s)
+      | ((Const c,ss),(Const d,ts))   => rigidrigid context (env,binders,c,d,ss,ts)
+      | ((Free(f),ss),(Free(g),ts))   => rigidrigid context (env,binders,f,g,ss,ts)
+      | ((Bound(i),ss),(Bound(j),ts)) => rigidrigidB context (env,binders,i,j,ss,ts)
       | ((Abs(_),_),_)                => raise Pattern
       | (_,(Abs(_),_))                => raise Pattern
-      | ((Const(c,_),_),(Free(f,_),_)) => (clash thy c f; raise Unif)
-      | ((Const(c,_),_),(Bound i,_))   => (clashB thy binders i c; raise Unif)
-      | ((Free(f,_),_),(Const(c,_),_)) => (clash thy f c; raise Unif)
-      | ((Free(f,_),_),(Bound i,_))    => (clashB thy binders i f; raise Unif)
-      | ((Bound i,_),(Const(c,_),_))   => (clashB thy binders i c; raise Unif)
-      | ((Bound i,_),(Free(f,_),_))    => (clashB thy binders i f; raise Unif)
+      | ((Const(c,_),_),(Free(f,_),_)) => (clash context c f; raise Unif)
+      | ((Const(c,_),_),(Bound i,_))   => (clashB context binders i c; raise Unif)
+      | ((Free(f,_),_),(Const(c,_),_)) => (clash context f c; raise Unif)
+      | ((Free(f,_),_),(Bound i,_))    => (clashB context binders i f; raise Unif)
+      | ((Bound i,_),(Const(c,_),_))   => (clashB context binders i c; raise Unif)
+      | ((Bound i,_),(Free(f,_),_))    => (clashB context binders i f; raise Unif)
 
 
-and rigidrigid thy (env,binders,(a,Ta),(b,Tb),ss,ts) =
-      if a<>b then (clash thy a b; raise Unif)
-      else env |> unify_types thy (Ta,Tb) |> fold (unif thy binders) (ss~~ts)
+and rigidrigid context (env,binders,(a,Ta),(b,Tb),ss,ts) =
+      if a<>b then (clash context a b; raise Unif)
+      else env |> unify_types context (Ta,Tb) |> fold (unif context binders) (ss~~ts)
 
-and rigidrigidB thy (env,binders,i,j,ss,ts) =
-     if i <> j then (clashBB thy binders i j; raise Unif)
-     else fold (unif thy binders) (ss~~ts) env
+and rigidrigidB context (env,binders,i,j,ss,ts) =
+     if i <> j then (clashBB context binders i j; raise Unif)
+     else fold (unif context binders) (ss~~ts) env
 
-and flexrigid thy (params as (env,binders,F,Fty,is,t)) =
-      if occurs(F,t,env) then (ocheck_fail thy (F,t,binders,env); raise Unif)
+and flexrigid context (params as (env,binders,F,Fty,is,t)) =
+      if occurs(F,t,env) then (ocheck_fail context (F,t,binders,env); raise Unif)
       else (let val (u,env') = proj(t,env,binders,is)
             in Envir.update ((F, Fty), mkabs (binders, is, u)) env' end
-            handle Unif => (proj_fail thy params; raise Unif));
+            handle Unif => (proj_fail context params; raise Unif));
 
-fun unify thy = unif thy [];
+fun unify context = unif context [];
 
 
 

--- a/src/Pure/raw_simplifier.ML	Sat Nov 08 17:39:01 2014 +0100
+++ b/src/Pure/raw_simplifier.ML	Sat Nov 08 21:31:51 2014 +0100
@@ -1306,7 +1306,7 @@
     val _ =
       cond_tracing ctxt (fn () =>
         print_term ctxt "SIMPLIFIER INVOKED ON THE FOLLOWING TERM:" (term_of ct));
-  in bottomc (mode, Option.map Drule.flexflex_unique oo prover, maxidx) ctxt ct end;
+  in bottomc (mode, Option.map (Drule.flexflex_unique (SOME ctxt)) oo prover, maxidx) ctxt ct end;
 
 val simple_prover =
   SINGLE o (fn ctxt => ALLGOALS (resolve_tac (prems_of ctxt)));

--- a/src/Pure/subgoal.ML	Sat Nov 08 17:39:01 2014 +0100
+++ b/src/Pure/subgoal.ML	Sat Nov 08 21:31:51 2014 +0100
@@ -126,7 +126,7 @@
       |> Thm.adjust_maxidx_thm idx
       |> singleton (Variable.export ctxt2 ctxt0);
   in
-    Thm.bicompose {flatten = true, match = false, incremented = false}
+    Thm.bicompose (SOME ctxt0) {flatten = true, match = false, incremented = false}
       (false, result, Thm.nprems_of st1) i st0
   end;
 

--- a/src/Pure/tactic.ML	Sat Nov 08 17:39:01 2014 +0100
+++ b/src/Pure/tactic.ML	Sat Nov 08 21:31:51 2014 +0100
@@ -28,7 +28,7 @@
   val match_tac: thm list -> int -> tactic
   val ematch_tac: thm list -> int -> tactic
   val dmatch_tac: thm list -> int -> tactic
-  val flexflex_tac: tactic
+  val flexflex_tac: Proof.context -> tactic
   val distinct_subgoal_tac: int -> tactic
   val distinct_subgoals_tac: tactic
   val cut_tac: thm -> int -> tactic
@@ -101,7 +101,7 @@
      thus (REPEAT (resolve_tac rules i)) stops once subgoal i disappears. *)
 
 (*Solve subgoal i by assumption*)
-fun assume_tac i = PRIMSEQ (Thm.assumption i);
+fun assume_tac i = PRIMSEQ (Thm.assumption NONE i);
 
 (*Solve subgoal i by assumption, using no unification*)
 fun eq_assume_tac i = PRIMITIVE (Thm.eq_assumption i);
@@ -112,14 +112,14 @@
 (*The composition rule/state: no lifting or var renaming.
   The arg = (bires_flg, orule, m);  see Thm.bicompose for explanation.*)
 fun compose_tac arg i =
-  PRIMSEQ (Thm.bicompose {flatten = true, match = false, incremented = false} arg i);
+  PRIMSEQ (Thm.bicompose NONE {flatten = true, match = false, incremented = false} arg i);
 
 (*Converts a "destruct" rule like P&Q==>P to an "elimination" rule
   like [| P&Q; P==>R |] ==> R *)
 fun make_elim rl = zero_var_indexes (rl RS revcut_rl);
 
 (*Attack subgoal i by resolution, using flags to indicate elimination rules*)
-fun biresolve_tac brules i = PRIMSEQ (Thm.biresolution false brules i);
+fun biresolve_tac brules i = PRIMSEQ (Thm.biresolution NONE false brules i);
 
 (*Resolution: the simple case, works for introduction rules*)
 fun resolve_tac rules = biresolve_tac (map (pair false) rules);
@@ -146,13 +146,13 @@
 fun solve_tac rules = resolve_tac rules THEN_ALL_NEW assume_tac;
 
 (*Matching tactics -- as above, but forbid updating of state*)
-fun bimatch_tac brules i = PRIMSEQ (Thm.biresolution true brules i);
+fun bimatch_tac brules i = PRIMSEQ (Thm.biresolution NONE true brules i);
 fun match_tac rules  = bimatch_tac (map (pair false) rules);
 fun ematch_tac rules = bimatch_tac (map (pair true) rules);
 fun dmatch_tac rls   = ematch_tac (map make_elim rls);
 
 (*Smash all flex-flex disagreement pairs in the proof state.*)
-val flexflex_tac = PRIMSEQ Thm.flexflex_rule;
+fun flexflex_tac ctxt = PRIMSEQ (Thm.flexflex_rule (SOME ctxt));
 
 (*Remove duplicate subgoals.*)
 val permute_tac = PRIMITIVE oo Thm.permute_prems;
@@ -244,7 +244,7 @@
       let val hyps = Logic.strip_assums_hyp prem
           and concl = Logic.strip_assums_concl prem
           val kbrls = Net.unify_term inet concl @ maps (Net.unify_term enet) hyps
-      in PRIMSEQ (Thm.biresolution match (order kbrls) i) end);
+      in PRIMSEQ (Thm.biresolution NONE match (order kbrls) i) end);
 
 (*versions taking pre-built nets.  No filtering of brls*)
 val biresolve_from_nets_tac = biresolution_from_nets_tac order_list false;
@@ -269,15 +269,12 @@
 
 (*resolution using a net rather than rules; pred supports filt_resolve_tac*)
 fun filt_resolution_from_net_tac match pred net =
-  SUBGOAL
-    (fn (prem,i) =>
-      let val krls = Net.unify_term net (Logic.strip_assums_concl prem)
-      in
-         if pred krls
-         then PRIMSEQ
-                (Thm.biresolution match (map (pair false) (order_list krls)) i)
-         else no_tac
-      end);
+  SUBGOAL (fn (prem,i) =>
+    let val krls = Net.unify_term net (Logic.strip_assums_concl prem) in
+      if pred krls then
+        PRIMSEQ (Thm.biresolution NONE match (map (pair false) (order_list krls)) i)
+      else no_tac
+    end);
 
 (*Resolve the subgoal using the rules (making a net) unless too flexible,
    which means more than maxr rules are unifiable.      *)

--- a/src/Pure/thm.ML	Sat Nov 08 17:39:01 2014 +0100
+++ b/src/Pure/thm.ML	Sat Nov 08 21:31:51 2014 +0100
@@ -115,7 +115,7 @@
   val combination: thm -> thm -> thm
   val equal_intr: thm -> thm -> thm
   val equal_elim: thm -> thm -> thm
-  val flexflex_rule: thm -> thm Seq.seq
+  val flexflex_rule: Proof.context option -> thm -> thm Seq.seq
   val generalize: string list * string list -> int -> thm -> thm
   val instantiate: (ctyp * ctyp) list * (cterm * cterm) list -> thm -> thm
   val instantiate_cterm: (ctyp * ctyp) list * (cterm * cterm) list -> cterm -> cterm
@@ -128,15 +128,15 @@
   val legacy_freezeT: thm -> thm
   val lift_rule: cterm -> thm -> thm
   val incr_indexes: int -> thm -> thm
-  val assumption: int -> thm -> thm Seq.seq
+  val assumption: Proof.context option -> int -> thm -> thm Seq.seq
   val eq_assumption: int -> thm -> thm
   val rotate_rule: int -> int -> thm -> thm
   val permute_prems: int -> int -> thm -> thm
   val rename_params_rule: string list * int -> thm -> thm
   val rename_boundvars: term -> term -> thm -> thm
-  val bicompose: {flatten: bool, match: bool, incremented: bool} ->
+  val bicompose: Proof.context option -> {flatten: bool, match: bool, incremented: bool} ->
     bool * thm * int -> int -> thm -> thm Seq.seq
-  val biresolution: bool -> (bool * thm) list -> int -> thm -> thm Seq.seq
+  val biresolution: Proof.context option -> bool -> (bool * thm) list -> int -> thm -> thm Seq.seq
   val extern_oracles: Proof.context -> (Markup.T * xstring) list
   val add_oracle: binding * ('a -> cterm) -> theory -> (string * ('a -> thm)) * theory
 end;
@@ -415,6 +415,11 @@
         prop = prop})
   end;
 
+fun make_context NONE thy = Context.Theory thy
+  | make_context (SOME ctxt) thy =
+      if Theory.subthy (thy, Proof_Context.theory_of ctxt) then Context.Proof ctxt
+      else raise THEORY ("Bad context", [thy, Proof_Context.theory_of ctxt]);
+
 (*explicit weakening: maps |- B to A |- B*)
 fun weaken raw_ct th =
   let
@@ -989,8 +994,8 @@
   Instantiates the theorem and deletes trivial tpairs.  Resulting
   sequence may contain multiple elements if the tpairs are not all
   flex-flex.*)
-fun flexflex_rule (th as Thm (der, {thy, maxidx, shyps, hyps, tpairs, prop, ...})) =
-  Unify.smash_unifiers thy tpairs (Envir.empty maxidx)
+fun flexflex_rule opt_ctxt (th as Thm (der, {thy, maxidx, shyps, hyps, tpairs, prop, ...})) =
+  Unify.smash_unifiers (make_context opt_ctxt thy) tpairs (Envir.empty maxidx)
   |> Seq.map (fn env =>
       if Envir.is_empty env then th
       else
@@ -1304,9 +1309,10 @@
       prop = Logic.incr_indexes ([], i) prop});
 
 (*Solve subgoal Bi of proof state B1...Bn/C by assumption. *)
-fun assumption i state =
+fun assumption opt_ctxt i state =
   let
     val Thm (der, {thy, maxidx, shyps, hyps, ...}) = state;
+    val context = make_context opt_ctxt thy;
     val (tpairs, Bs, Bi, C) = dest_state (state, i);
     fun newth n (env, tpairs) =
       Thm (deriv_rule1
@@ -1332,7 +1338,7 @@
       | addprfs (asm :: rest) n = Seq.make (fn () => Seq.pull
           (Seq.mapp (newth n)
             (if Term.could_unify (asm, concl) then
-              (Unify.unifiers (thy, Envir.empty maxidx, (close asm, concl') :: tpairs))
+              (Unify.unifiers (context, Envir.empty maxidx, (close asm, concl') :: tpairs))
              else Seq.empty)
             (addprfs rest (n + 1))))
   in addprfs asms 1 end;
@@ -1555,9 +1561,9 @@
 
 
 (*unify types of schematic variables (non-lifted case)*)
-fun unify_var_types thy (th1, th2) env =
+fun unify_var_types context (th1, th2) env =
   let
-    fun unify_vars (T :: Us) = fold (fn U => Pattern.unify_types thy (T, U)) Us
+    fun unify_vars (T :: Us) = fold (fn U => Pattern.unify_types context (T, U)) Us
       | unify_vars _ = I;
     val add_vars =
       full_prop_of #>
@@ -1576,7 +1582,7 @@
 *)
 local exception COMPOSE
 in
-fun bicompose_aux {flatten, match, incremented} (state, (stpairs, Bs, Bi, C), lifted)
+fun bicompose_aux opt_ctxt {flatten, match, incremented} (state, (stpairs, Bs, Bi, C), lifted)
                         (eres_flg, orule, nsubgoal) =
  let val Thm (sder, {maxidx=smax, shyps=sshyps, hyps=shyps, ...}) = state
      and Thm (rder, {maxidx=rmax, shyps=rshyps, hyps=rhyps,
@@ -1584,6 +1590,7 @@
          (*How many hyps to skip over during normalization*)
      and nlift = Logic.count_prems (strip_all_body Bi) + (if eres_flg then ~1 else 0)
      val thy = merge_thys2 state orule;
+     val context = make_context opt_ctxt thy;
      (** Add new theorem with prop = '[| Bs; As |] ==> C' to thq **)
      fun addth A (As, oldAs, rder', n) ((env, tpairs), thq) =
        let val normt = Envir.norm_term env;
@@ -1646,7 +1653,7 @@
                | tryasms (asm :: rest) n =
                    if Term.could_unify (asm, concl) then
                      let val asm' = close asm in
-                       (case Seq.pull (Unify.unifiers (thy, env, (asm', concl') :: dpairs)) of
+                       (case Seq.pull (Unify.unifiers (context, env, (asm', concl') :: dpairs)) of
                          NONE => tryasms rest (n + 1)
                        | cell as SOME ((_, tpairs), _) =>
                            Seq.it_right (addth A (newAs (As, n, [BBi, (concl', asm')], tpairs)))
@@ -1658,7 +1665,7 @@
 
      (*ordinary resolution*)
      fun res env =
-       (case Seq.pull (Unify.unifiers (thy, env, dpairs)) of
+       (case Seq.pull (Unify.unifiers (context, env, dpairs)) of
          NONE => Seq.empty
        | cell as SOME ((_, tpairs), _) =>
            Seq.it_right (addth NONE (newAs (rev rAs, 0, [BBi], tpairs)))
@@ -1666,14 +1673,14 @@
 
      val env0 = Envir.empty (Int.max (rmax, smax));
  in
-   (case if incremented then SOME env0 else unify_var_types thy (state, orule) env0 of
+   (case if incremented then SOME env0 else unify_var_types context (state, orule) env0 of
      NONE => Seq.empty
    | SOME env => if eres_flg then eres env (rev rAs) else res env)
  end;
 end;
 
-fun bicompose flags arg i state =
-  bicompose_aux flags (state, dest_state (state,i), false) arg;
+fun bicompose opt_ctxt flags arg i state =
+  bicompose_aux opt_ctxt flags (state, dest_state (state,i), false) arg;
 
 (*Quick test whether rule is resolvable with the subgoal with hyps Hs
   and conclusion B.  If eres_flg then checks 1st premise of rule also*)
@@ -1686,18 +1693,18 @@
 
 (*Bi-resolution of a state with a list of (flag,rule) pairs.
   Puts the rule above:  rule/state.  Renames vars in the rules. *)
-fun biresolution match brules i state =
+fun biresolution opt_ctxt match brules i state =
     let val (stpairs, Bs, Bi, C) = dest_state(state,i);
         val lift = lift_rule (cprem_of state i);
         val B = Logic.strip_assums_concl Bi;
         val Hs = Logic.strip_assums_hyp Bi;
         val compose =
-          bicompose_aux {flatten = true, match = match, incremented = true}
+          bicompose_aux opt_ctxt {flatten = true, match = match, incremented = true}
             (state, (stpairs, Bs, Bi, C), true);
         fun res [] = Seq.empty
           | res ((eres_flg, rule)::brules) =
-              if Config.get_global (theory_of_thm state) Pattern.unify_trace_failure orelse
-                 could_bires (Hs, B, eres_flg, rule)
+              if Config.get_generic (make_context opt_ctxt (theory_of_thm state))
+                  Pattern.unify_trace_failure orelse could_bires (Hs, B, eres_flg, rule)
               then Seq.make (*delay processing remainder till needed*)
                   (fn()=> SOME(compose (eres_flg, lift rule, nprems_of rule),
                                res brules))

--- a/src/Pure/unify.ML	Sat Nov 08 17:39:01 2014 +0100
+++ b/src/Pure/unify.ML	Sat Nov 08 21:31:51 2014 +0100
@@ -19,13 +19,13 @@
   val trace_simp: bool Config.T
   val trace_types_raw: Config.raw
   val trace_types: bool Config.T
-  val hounifiers: theory * Envir.env * ((term * term) list) ->
+  val hounifiers: Context.generic * Envir.env * ((term * term) list) ->
     (Envir.env * (term * term) list) Seq.seq
-  val unifiers: theory * Envir.env * ((term * term) list) ->
+  val unifiers: Context.generic * Envir.env * ((term * term) list) ->
     (Envir.env * (term * term) list) Seq.seq
-  val smash_unifiers: theory -> (term * term) list -> Envir.env -> Envir.env Seq.seq
-  val matchers: theory -> (term * term) list -> Envir.env Seq.seq
-  val matches_list: theory -> term list -> term list -> bool
+  val smash_unifiers: Context.generic -> (term * term) list -> Envir.env -> Envir.env Seq.seq
+  val matchers: Context.generic -> (term * term) list -> Envir.env Seq.seq
+  val matches_list: Context.generic -> term list -> term list -> bool
 end
 
 structure Unify : UNIFY =
@@ -34,19 +34,19 @@
 (*Unification options*)
 
 (*tracing starts above this depth, 0 for full*)
-val trace_bound_raw = Config.declare_global ("unify_trace_bound", @{here}) (K (Config.Int 50));
+val trace_bound_raw = Config.declare ("unify_trace_bound", @{here}) (K (Config.Int 50));
 val trace_bound = Config.int trace_bound_raw;
 
 (*unification quits above this depth*)
-val search_bound_raw = Config.declare_global ("unify_search_bound", @{here}) (K (Config.Int 60));
+val search_bound_raw = Config.declare ("unify_search_bound", @{here}) (K (Config.Int 60));
 val search_bound = Config.int search_bound_raw;
 
 (*print dpairs before calling SIMPL*)
-val trace_simp_raw = Config.declare_global ("unify_trace_simp", @{here}) (K (Config.Bool false));
+val trace_simp_raw = Config.declare ("unify_trace_simp", @{here}) (K (Config.Bool false));
 val trace_simp = Config.bool trace_simp_raw;
 
 (*announce potential incompleteness of type unification*)
-val trace_types_raw = Config.declare_global ("unify_trace_types", @{here}) (K (Config.Bool false));
+val trace_types_raw = Config.declare ("unify_trace_types", @{here}) (K (Config.Bool false));
 val trace_types = Config.bool trace_types_raw;
 
 
@@ -183,18 +183,18 @@
 exception ASSIGN;  (*Raised if not an assignment*)
 
 
-fun unify_types thy TU env =
-  Pattern.unify_types thy TU env handle Pattern.Unif => raise CANTUNIFY;
+fun unify_types context TU env =
+  Pattern.unify_types context TU env handle Pattern.Unif => raise CANTUNIFY;
 
-fun test_unify_types thy (T, U) env =
+fun test_unify_types context (T, U) env =
   let
-    val str_of = Syntax.string_of_typ_global thy;
-    fun warn () =
-      if Context_Position.is_visible_global thy then
-        tracing ("Potential loss of completeness: " ^ str_of U ^ " = " ^ str_of T)
+    fun trace () =
+      if Context_Position.is_visible_generic context then
+        let val str_of = Syntax.string_of_typ (Context.proof_of context)
+        in tracing ("Potential loss of completeness: " ^ str_of U ^ " = " ^ str_of T) end
       else ();
-    val env' = unify_types thy (T, U) env;
-  in if is_TVar T orelse is_TVar U then warn () else (); env' end;
+    val env' = unify_types context (T, U) env;
+  in if is_TVar T orelse is_TVar U then trace () else (); env' end;
 
 (*Is the term eta-convertible to a single variable with the given rbinder?
   Examples: ?a   ?f(B.0)   ?g(B.1,B.0)
@@ -209,11 +209,11 @@
 (*Solve v=u by assignment -- "fixedpoint" to Huet -- if v not in u.
   If v occurs rigidly then nonunifiable.
   If v occurs nonrigidly then must use full algorithm. *)
-fun assignment thy (rbinder, t, u) env =
+fun assignment context (rbinder, t, u) env =
   let val vT as (v,T) = get_eta_var (rbinder, 0, t) in
     (case rigid_occurs_term (Unsynchronized.ref [], env, v, u) of
       NoOcc =>
-        let val env = unify_types thy (Envir.body_type env T, fastype env (rbinder, u)) env
+        let val env = unify_types context (Envir.body_type env T, fastype env (rbinder, u)) env
         in Envir.update (vT, Logic.rlist_abs (rbinder, u)) env end
     | Nonrigid => raise ASSIGN
     | Rigid => raise CANTUNIFY)
@@ -225,18 +225,18 @@
   Checks that binders have same length, since terms should be eta-normal;
     if not, raises TERM, probably indicating type mismatch.
   Uses variable a (unless the null string) to preserve user's naming.*)
-fun new_dpair thy (rbinder, Abs (a, T, body1), Abs (b, U, body2)) env =
+fun new_dpair context (rbinder, Abs (a, T, body1), Abs (b, U, body2)) env =
       let
-        val env' = unify_types thy (T, U) env;
+        val env' = unify_types context (T, U) env;
         val c = if a = "" then b else a;
-      in new_dpair thy ((c,T) :: rbinder, body1, body2) env' end
+      in new_dpair context ((c,T) :: rbinder, body1, body2) env' end
   | new_dpair _ (_, Abs _, _) _ = raise TERM ("new_dpair", [])
   | new_dpair _ (_, _, Abs _) _ = raise TERM ("new_dpair", [])
   | new_dpair _ (rbinder, t1, t2) env = ((rbinder, t1, t2), env);
 
 
-fun head_norm_dpair thy (env, (rbinder, t, u)) : dpair * Envir.env =
-  new_dpair thy (rbinder,
+fun head_norm_dpair context (env, (rbinder, t, u)) : dpair * Envir.env =
+  new_dpair context (rbinder,
     eta_norm env (rbinder, Envir.head_norm env t),
     eta_norm env (rbinder, Envir.head_norm env u)) env;
 
@@ -248,11 +248,11 @@
   Does not even identify Vars in dpairs such as ?a =?= ?b; an attempt to
     do so caused numerous problems with no compensating advantage.
 *)
-fun SIMPL0 thy dp0 (env,flexflex,flexrigid) : Envir.env * dpair list * dpair list =
+fun SIMPL0 context dp0 (env,flexflex,flexrigid) : Envir.env * dpair list * dpair list =
   let
-    val (dp as (rbinder, t, u), env) = head_norm_dpair thy (env, dp0);
+    val (dp as (rbinder, t, u), env) = head_norm_dpair context (env, dp0);
     fun SIMRANDS (f $ t, g $ u, env) =
-          SIMPL0 thy (rbinder, t, u) (SIMRANDS (f, g, env))
+          SIMPL0 context (rbinder, t, u) (SIMRANDS (f, g, env))
       | SIMRANDS (t as _$_, _, _) =
           raise TERM ("SIMPL: operands mismatch", [t, u])
       | SIMRANDS (t, u as _ $ _, _) =
@@ -263,21 +263,21 @@
       (Var (_, T), Var (_, U)) =>
         let
           val T' = Envir.body_type env T and U' = Envir.body_type env U;
-          val env = unify_types thy (T', U') env;
+          val env = unify_types context (T', U') env;
         in (env, dp :: flexflex, flexrigid) end
     | (Var _, _) =>
-        ((assignment thy (rbinder,t,u) env, flexflex, flexrigid)
+        ((assignment context (rbinder,t,u) env, flexflex, flexrigid)
           handle ASSIGN => (env, flexflex, dp :: flexrigid))
     | (_, Var _) =>
-        ((assignment thy (rbinder, u, t) env, flexflex, flexrigid)
+        ((assignment context (rbinder, u, t) env, flexflex, flexrigid)
           handle ASSIGN => (env, flexflex, (rbinder, u, t) :: flexrigid))
     | (Const (a, T), Const (b, U)) =>
-        if a = b then SIMRANDS (t, u, unify_types thy (T, U) env)
+        if a = b then SIMRANDS (t, u, unify_types context (T, U) env)
         else raise CANTUNIFY
     | (Bound i, Bound j) =>
         if i = j then SIMRANDS (t, u, env) else raise CANTUNIFY
     | (Free (a, T), Free (b, U)) =>
-        if a = b then SIMRANDS (t, u, unify_types thy (T, U) env)
+        if a = b then SIMRANDS (t, u, unify_types context (T, U) env)
         else raise CANTUNIFY
     | _ => raise CANTUNIFY)
   end;
@@ -291,13 +291,13 @@
 
 (*Recursion needed if any of the 'head variables' have been updated
   Clever would be to re-do just the affected dpairs*)
-fun SIMPL thy (env,dpairs) : Envir.env * dpair list * dpair list =
+fun SIMPL context (env,dpairs) : Envir.env * dpair list * dpair list =
   let
-    val all as (env', flexflex, flexrigid) = fold_rev (SIMPL0 thy) dpairs (env, [], []);
+    val all as (env', flexflex, flexrigid) = fold_rev (SIMPL0 context) dpairs (env, [], []);
     val dps = flexrigid @ flexflex;
   in
     if exists (fn (_, t, u) => changed env' t orelse changed env' u) dps
-    then SIMPL thy (env', dps) else all
+    then SIMPL context (env', dps) else all
   end;
 
 
@@ -331,11 +331,11 @@
   For example, projection in ?b'(?a) may be wrong if other dpairs constrain ?a.
   The order for trying projections is crucial in ?b'(?a)
   NB "vname" is only used in the call to make_args!!   *)
-fun matchcopy thy vname =
+fun matchcopy context vname =
   let
     fun mc (rbinder, targs, u, ed as (env, dpairs)) : (term * (Envir.env * dpair list)) Seq.seq =
       let
-        val trace_types = Config.get_global thy trace_types;
+        val trace_types = Config.get_generic context trace_types;
         (*Produce copies of uarg and cons them in front of uargs*)
         fun copycons uarg (uargs, (env, dpairs)) =
           Seq.map (fn (uarg', ed') => (uarg' :: uargs, ed'))
@@ -352,8 +352,8 @@
         fun projenv (head, (Us, bary), targ, tail) =
           let
             val env =
-              if trace_types then test_unify_types thy (base, bary) env
-              else unify_types thy (base, bary) env
+              if trace_types then test_unify_types context (base, bary) env
+              else unify_types context (base, bary) env
           in
             Seq.make (fn () =>
               let
@@ -361,7 +361,7 @@
                 (*higher-order projection: plug in targs for bound vars*)
                 fun plugin arg = list_comb (head_of arg, targs);
                 val dp = (rbinder, list_comb (targ, map plugin args), u);
-                val (env2, frigid, fflex) = SIMPL thy (env', dp :: dpairs);
+                val (env2, frigid, fflex) = SIMPL context (env', dp :: dpairs);
                 (*may raise exception CANTUNIFY*)
               in
                 SOME ((list_comb (head, args), (env2, frigid @ fflex)), tail)
@@ -398,7 +398,7 @@
 
 
 (*Call matchcopy to produce assignments to the variable in the dpair*)
-fun MATCH thy (env, (rbinder, t, u), dpairs) : (Envir.env * dpair list) Seq.seq =
+fun MATCH context (env, (rbinder, t, u), dpairs) : (Envir.env * dpair list) Seq.seq =
   let
     val (Var (vT as (v, T)), targs) = strip_comb t;
     val Ts = Envir.binder_types env T;
@@ -408,7 +408,7 @@
         NONE => (Envir.update (vT, types_abs (Ts, u')) env', dpairs')
       | SOME s => (env', ([], s, types_abs (Ts, u')) :: dpairs'));
   in
-    Seq.map new_dset (matchcopy thy (#1 v) (rbinder, targs, u, (env, dpairs)))
+    Seq.map new_dset (matchcopy context (#1 v) (rbinder, targs, u, (env, dpairs)))
   end;
 
 
@@ -417,11 +417,11 @@
 
 (*At end of unification, do flex-flex assignments like ?a -> ?f(?b)
   Attempts to update t with u, raising ASSIGN if impossible*)
-fun ff_assign thy (env, rbinder, t, u) : Envir.env =
+fun ff_assign context (env, rbinder, t, u) : Envir.env =
   let val vT as (v, T) = get_eta_var (rbinder, 0, t) in
     if occurs_terms (Unsynchronized.ref [], env, v, [u]) then raise ASSIGN
     else
-      let val env = unify_types thy (Envir.body_type env T, fastype env (rbinder, u)) env
+      let val env = unify_types context (Envir.body_type env T, fastype env (rbinder, u)) env
       in Envir.vupdate (vT, Logic.rlist_abs (rbinder, u)) env end
   end;
 
@@ -531,7 +531,7 @@
 
 (*Simplify both terms and check for assignments.
   Bound vars in the binder are "banned" unless used in both t AND u *)
-fun clean_ffpair thy ((rbinder, t, u), (env, tpairs)) =
+fun clean_ffpair context ((rbinder, t, u), (env, tpairs)) =
   let
     val loot = loose_bnos t and loou = loose_bnos u
     fun add_index (j, (a, T)) (bnos, newbinder) =
@@ -542,9 +542,9 @@
     val (env', t') = clean_term banned (env, t);
     val (env'',u') = clean_term banned (env',u);
   in
-    (ff_assign thy (env'', rbin', t', u'), tpairs)
+    (ff_assign context (env'', rbin', t', u'), tpairs)
       handle ASSIGN =>
-        (ff_assign thy (env'', rbin', u', t'), tpairs)
+        (ff_assign context (env'', rbin', u', t'), tpairs)
           handle ASSIGN => (env'', add_tpair (rbin', (t', u'), tpairs))
   end
   handle CHANGE_FAIL => (env, add_tpair (rbinder, (t, u), tpairs));
@@ -554,7 +554,7 @@
   eliminates trivial tpairs like t=t, as well as repeated ones
   trivial tpairs can easily escape SIMPL:  ?A=t, ?A=?B, ?B=t gives t=t
   Resulting tpairs MAY NOT be in normal form:  assignments may occur here.*)
-fun add_ffpair thy (rbinder,t0,u0) (env,tpairs) : Envir.env * (term * term) list =
+fun add_ffpair context (rbinder,t0,u0) (env,tpairs) : Envir.env * (term * term) list =
   let
     val t = Envir.norm_term env t0
     and u = Envir.norm_term env u0;
@@ -565,8 +565,8 @@
           if T = U then (env, add_tpair (rbinder, (t, u), tpairs))
           else raise TERM ("add_ffpair: Var name confusion", [t, u])
         else if Term_Ord.indexname_ord (v, w) = LESS then (*prefer to update the LARGER variable*)
-          clean_ffpair thy ((rbinder, u, t), (env, tpairs))
-        else clean_ffpair thy ((rbinder, t, u), (env, tpairs))
+          clean_ffpair context ((rbinder, u, t), (env, tpairs))
+        else clean_ffpair context ((rbinder, t, u), (env, tpairs))
     | _ => raise TERM ("add_ffpair: Vars expected", [t, u]))
   end;
 
@@ -574,15 +574,16 @@
 (*Print a tracing message + list of dpairs.
   In t==u print u first because it may be rigid or flexible --
     t is always flexible.*)
-fun print_dpairs thy msg (env, dpairs) =
-  if Context_Position.is_visible_global thy then
+fun print_dpairs context msg (env, dpairs) =
+  if Context_Position.is_visible_generic context then
     let
       fun pdp (rbinder, t, u) =
         let
+          val ctxt = Context.proof_of context;
           fun termT t =
-            Syntax.pretty_term_global thy (Envir.norm_term env (Logic.rlist_abs (rbinder, t)));
-          val bsymbs = [termT u, Pretty.str " =?=", Pretty.brk 1, termT t];
-        in tracing (Pretty.string_of (Pretty.blk (0, bsymbs))) end;
+            Syntax.pretty_term ctxt (Envir.norm_term env (Logic.rlist_abs (rbinder, t)));
+          val prt = Pretty.blk (0, [termT u, Pretty.str " =?=", Pretty.brk 1, termT t]);
+        in tracing (Pretty.string_of prt) end;
     in tracing msg; List.app pdp dpairs end
   else ();
 
@@ -590,41 +591,41 @@
 (*Unify the dpairs in the environment.
   Returns flex-flex disagreement pairs NOT IN normal form.
   SIMPL may raise exception CANTUNIFY. *)
-fun hounifiers (thy, env, tus : (term * term) list) : (Envir.env * (term * term) list) Seq.seq =
+fun hounifiers (context, env, tus : (term * term) list) : (Envir.env * (term * term) list) Seq.seq =
   let
-    val trace_bound = Config.get_global thy trace_bound;
-    val search_bound = Config.get_global thy search_bound;
-    val trace_simp = Config.get_global thy trace_simp;
+    val trace_bound = Config.get_generic context trace_bound;
+    val search_bound = Config.get_generic context search_bound;
+    val trace_simp = Config.get_generic context trace_simp;
     fun add_unify tdepth ((env, dpairs), reseq) =
       Seq.make (fn () =>
         let
           val (env', flexflex, flexrigid) =
            (if tdepth > trace_bound andalso trace_simp
-            then print_dpairs thy "Enter SIMPL" (env, dpairs) else ();
-            SIMPL thy (env, dpairs));
+            then print_dpairs context "Enter SIMPL" (env, dpairs) else ();
+            SIMPL context (env, dpairs));
         in
           (case flexrigid of
-            [] => SOME (fold_rev (add_ffpair thy) flexflex (env', []), reseq)
+            [] => SOME (fold_rev (add_ffpair context) flexflex (env', []), reseq)
           | dp :: frigid' =>
               if tdepth > search_bound then
-                (if Context_Position.is_visible_global thy
+                (if Context_Position.is_visible_generic context
                  then warning "Unification bound exceeded" else (); Seq.pull reseq)
               else
                (if tdepth > trace_bound then
-                  print_dpairs thy "Enter MATCH" (env',flexrigid@flexflex)
+                  print_dpairs context "Enter MATCH" (env',flexrigid@flexflex)
                 else ();
                 Seq.pull (Seq.it_right
-                    (add_unify (tdepth + 1)) (MATCH thy (env',dp, frigid'@flexflex), reseq))))
+                    (add_unify (tdepth + 1)) (MATCH context (env',dp, frigid'@flexflex), reseq))))
         end
         handle CANTUNIFY =>
-         (if tdepth > trace_bound andalso Context_Position.is_visible_global thy
+         (if tdepth > trace_bound andalso Context_Position.is_visible_generic context
           then tracing "Failure node"
           else (); Seq.pull reseq));
     val dps = map (fn (t, u) => ([], t, u)) tus;
   in add_unify 1 ((env, dps), Seq.empty) end;
 
-fun unifiers (params as (thy, env, tus)) =
-  Seq.cons (fold (Pattern.unify thy) tus env, []) Seq.empty
+fun unifiers (params as (context, env, tus)) =
+  Seq.cons (fold (Pattern.unify context) tus env, []) Seq.empty
     handle Pattern.Unif => Seq.empty
       | Pattern.Pattern => hounifiers params;
 
@@ -660,8 +661,8 @@
   fold_rev smash_flexflex1 tpairs env;
 
 (*Returns unifiers with no remaining disagreement pairs*)
-fun smash_unifiers thy tus env =
-  Seq.map smash_flexflex (unifiers (thy, env, tus));
+fun smash_unifiers context tus env =
+  Seq.map smash_flexflex (unifiers (context, env, tus));
 
 
 (*Pattern matching*)
@@ -672,8 +673,10 @@
 
 (*General matching -- keep variables disjoint*)
 fun matchers _ [] = Seq.single (Envir.empty ~1)
-  | matchers thy pairs =
+  | matchers context pairs =
       let
+        val thy = Context.theory_of context;
+
         val maxidx = fold (Term.maxidx_term o #2) pairs ~1;
         val offset = maxidx + 1;
         val pairs' = map (apfst (Logic.incr_indexes ([], offset))) pairs;
@@ -719,11 +722,11 @@
         val empty = Envir.empty maxidx';
       in
         Seq.append
-          (Seq.map_filter result (smash_unifiers thy pairs' empty))
+          (Seq.map_filter result (smash_unifiers context pairs' empty))
           (first_order_matchers thy pairs empty)
       end;
 
-fun matches_list thy ps os =
-  length ps = length os andalso is_some (Seq.pull (matchers thy (ps ~~ os)));
+fun matches_list context ps os =
+  length ps = length os andalso is_some (Seq.pull (matchers context (ps ~~ os)));
 
 end;

--- a/src/Tools/eqsubst.ML	Sat Nov 08 17:39:01 2014 +0100
+++ b/src/Tools/eqsubst.ML	Sat Nov 08 21:31:51 2014 +0100
@@ -161,7 +161,7 @@
              Vartab.dest (Envir.term_env env));
           val initenv =
             Envir.Envir {maxidx = ix2, tenv = Vartab.empty, tyenv = typinsttab};
-          val useq = Unify.smash_unifiers thy [a] initenv
+          val useq = Unify.smash_unifiers (Context.Theory thy) [a] initenv
             handle ListPair.UnequalLengths => Seq.empty
               | Term.TERM _ => Seq.empty;
           fun clean_unify' useq () =

--- a/src/Tools/induct.ML	Sat Nov 08 17:39:01 2014 +0100
+++ b/src/Tools/induct.ML	Sat Nov 08 21:31:51 2014 +0100
@@ -602,7 +602,8 @@
         val rule' = Thm.incr_indexes (maxidx + 1) rule;
         val concl = Logic.strip_assums_concl goal;
       in
-        Unify.smash_unifiers thy [(Thm.concl_of rule', concl)] (Envir.empty (Thm.maxidx_of rule'))
+        Unify.smash_unifiers (Context.Proof ctxt)
+          [(Thm.concl_of rule', concl)] (Envir.empty (Thm.maxidx_of rule'))
         |> Seq.map (fn env => Drule.instantiate_normalize (dest_env thy env) rule')
       end
   end

--- a/src/Tools/misc_legacy.ML	Sat Nov 08 17:39:01 2014 +0100
+++ b/src/Tools/misc_legacy.ML	Sat Nov 08 21:31:51 2014 +0100
@@ -204,7 +204,7 @@
         end
       (*function to replace the current subgoal*)
       fun next st =
-        Thm.bicompose {flatten = true, match = false, incremented = false}
+        Thm.bicompose NONE {flatten = true, match = false, incremented = false}
           (false, relift st, nprems_of st) gno state
   in Seq.maps next (tacf subprems (Thm.trivial (cterm concl))) end;