optional proof context for unify operations, for the sake of proper local options;
authorwenzelm
Sat Nov 08 21:31:51 2014 +0100 (2014-11-08)
changeset 58950d07464875dd4
parent 58949 e9559088ba29
child 58951 8b7caf447357
optional proof context for unify operations, for the sake of proper local options;
src/Doc/Implementation/Tactic.thy
src/HOL/Nominal/nominal_fresh_fun.ML
src/HOL/TLA/Intensional.thy
src/HOL/Tools/Function/function_core.ML
src/HOL/Tools/Function/induction_schema.ML
src/HOL/Tools/Metis/metis_reconstruct.ML
src/HOL/Tools/Predicate_Compile/predicate_compile_specialisation.ML
src/HOL/Tools/Quotient/quotient_tacs.ML
src/HOL/Tools/TFL/casesplit.ML
src/Provers/blast.ML
src/Provers/classical.ML
src/Provers/hypsubst.ML
src/Pure/Isar/calculation.ML
src/Pure/Isar/method.ML
src/Pure/Isar/proof.ML
src/Pure/Isar/proof_context.ML
src/Pure/Isar/rule_cases.ML
src/Pure/Proof/extraction.ML
src/Pure/Proof/reconstruct.ML
src/Pure/Tools/rule_insts.ML
src/Pure/drule.ML
src/Pure/goal.ML
src/Pure/par_tactical.ML
src/Pure/pattern.ML
src/Pure/raw_simplifier.ML
src/Pure/subgoal.ML
src/Pure/tactic.ML
src/Pure/thm.ML
src/Pure/unify.ML
src/Tools/eqsubst.ML
src/Tools/induct.ML
src/Tools/misc_legacy.ML
     1.1 --- a/src/Doc/Implementation/Tactic.thy	Sat Nov 08 17:39:01 2014 +0100
     1.2 +++ b/src/Doc/Implementation/Tactic.thy	Sat Nov 08 21:31:51 2014 +0100
     1.3 @@ -454,7 +454,7 @@
     1.4    \begin{mldecls}
     1.5    @{index_ML rotate_tac: "int -> int -> tactic"} \\
     1.6    @{index_ML distinct_subgoals_tac: tactic} \\
     1.7 -  @{index_ML flexflex_tac: tactic} \\
     1.8 +  @{index_ML flexflex_tac: "Proof.context -> tactic"} \\
     1.9    \end{mldecls}
    1.10  
    1.11    \begin{description}
     2.1 --- a/src/HOL/Nominal/nominal_fresh_fun.ML	Sat Nov 08 17:39:01 2014 +0100
     2.2 +++ b/src/HOL/Nominal/nominal_fresh_fun.ML	Sat Nov 08 21:31:51 2014 +0100
     2.3 @@ -37,8 +37,8 @@
     2.4  val res_inst_tac_term' =
     2.5    gen_res_inst_tac_term (K Drule.cterm_instantiate) [];
     2.6  
     2.7 -fun cut_inst_tac_term' tinst th =
     2.8 -  res_inst_tac_term' tinst false (Rule_Insts.make_elim_preserve th);
     2.9 +fun cut_inst_tac_term' ctxt tinst th =
    2.10 +  res_inst_tac_term' tinst false (Rule_Insts.make_elim_preserve ctxt th);
    2.11  
    2.12  fun get_dyn_thm thy name atom_name =
    2.13    Global_Theory.get_thm thy name handle ERROR _ =>
    2.14 @@ -76,7 +76,7 @@
    2.15     val x = hd (Misc_Legacy.term_vars (prop_of exists_fresh'));
    2.16   in
    2.17     fn st =>
    2.18 -   (cut_inst_tac_term' [(x,s)] exists_fresh' 1 THEN
    2.19 +   (cut_inst_tac_term' ctxt [(x,s)] exists_fresh' 1 THEN
    2.20     rtac fs_name_thm 1 THEN
    2.21     etac exE 1) st
    2.22    handle List.Empty  => all_tac st (* if we collected no variables then we do nothing *)
     3.1 --- a/src/HOL/TLA/Intensional.thy	Sat Nov 08 17:39:01 2014 +0100
     3.2 +++ b/src/HOL/TLA/Intensional.thy	Sat Nov 08 21:31:51 2014 +0100
     3.3 @@ -262,7 +262,7 @@
     3.4    let
     3.5      (* analogous to RS, but using matching instead of resolution *)
     3.6      fun matchres tha i thb =
     3.7 -      case Seq.chop 2 (Thm.biresolution true [(false,tha)] i thb) of
     3.8 +      case Seq.chop 2 (Thm.biresolution NONE true [(false,tha)] i thb) of
     3.9            ([th],_) => th
    3.10          | ([],_)   => raise THM("matchres: no match", i, [tha,thb])
    3.11          |      _   => raise THM("matchres: multiple unifiers", i, [tha,thb])
     4.1 --- a/src/HOL/Tools/Function/function_core.ML	Sat Nov 08 17:39:01 2014 +0100
     4.2 +++ b/src/HOL/Tools/Function/function_core.ML	Sat Nov 08 21:31:51 2014 +0100
     4.3 @@ -351,7 +351,8 @@
     4.4        map2 (mk_uniqueness_clause thy globals compat_store clausei) clauses rep_lemmas
     4.5  
     4.6      fun elim_implies_eta A AB =
     4.7 -      Thm.bicompose {flatten = false, match = true, incremented = false} (false, A, 0) 1 AB
     4.8 +      Thm.bicompose (SOME ctxt) {flatten = false, match = true, incremented = false}
     4.9 +        (false, A, 0) 1 AB
    4.10        |> Seq.list_of |> the_single
    4.11  
    4.12      val uniqueness = G_cases
     5.1 --- a/src/HOL/Tools/Function/induction_schema.ML	Sat Nov 08 17:39:01 2014 +0100
     5.2 +++ b/src/HOL/Tools/Function/induction_schema.ML	Sat Nov 08 21:31:51 2014 +0100
     5.3 @@ -387,7 +387,7 @@
     5.4      val nbranches = length branches
     5.5      val npres = length pres
     5.6    in
     5.7 -    Thm.bicompose {flatten = false, match = false, incremented = false}
     5.8 +    Thm.bicompose (SOME ctxt') {flatten = false, match = false, incremented = false}
     5.9        (false, res, length newgoals) i
    5.10      THEN term_tac (i + nbranches + npres)
    5.11      THEN (EVERY (map (TRY o pres_tac) ((i + nbranches + npres - 1) downto (i + nbranches))))
     6.1 --- a/src/HOL/Tools/Metis/metis_reconstruct.ML	Sat Nov 08 17:39:01 2014 +0100
     6.2 +++ b/src/HOL/Tools/Metis/metis_reconstruct.ML	Sat Nov 08 21:31:51 2014 +0100
     6.3 @@ -187,7 +187,7 @@
     6.4    let
     6.5      val tha = incr_type_indexes (1 + Thm.maxidx_of thb) tha
     6.6      fun res (tha, thb) =
     6.7 -      (case Thm.bicompose {flatten = true, match = false, incremented = true}
     6.8 +      (case Thm.bicompose (SOME ctxt) {flatten = true, match = false, incremented = true}
     6.9              (false, tha, nprems_of tha) i thb
    6.10             |> Seq.list_of |> distinct Thm.eq_thm of
    6.11          [th] => th
    6.12 @@ -211,7 +211,7 @@
    6.13            |> AList.group (op =)
    6.14            |> maps (fn ((s, _), T :: Ts) => map (fn T' => (Free (s, T), Free (s, T'))) Ts)
    6.15            |> rpair (Envir.empty ~1)
    6.16 -          |-> fold (Pattern.unify thy)
    6.17 +          |-> fold (Pattern.unify (Context.Proof ctxt))
    6.18            |> Envir.type_env |> Vartab.dest
    6.19            |> map (fn (x, (S, T)) => pairself (ctyp_of thy) (TVar (x, S), T))
    6.20        in
    6.21 @@ -747,7 +747,7 @@
    6.22                THEN rotate_tac (rotation_of_subgoal i) i
    6.23                THEN PRIMITIVE (unify_first_prem_with_concl thy i)
    6.24                THEN assume_tac i
    6.25 -              THEN flexflex_tac)))
    6.26 +              THEN flexflex_tac ctxt')))
    6.27        handle ERROR msg =>
    6.28          cat_error msg
    6.29            "Cannot replay Metis proof in Isabelle: error when discharging Skolem assumptions"
     7.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_specialisation.ML	Sat Nov 08 17:39:01 2014 +0100
     7.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_specialisation.ML	Sat Nov 08 21:31:51 2014 +0100
     7.3 @@ -83,7 +83,7 @@
     7.4      fun specialise_intro intro =
     7.5        (let
     7.6          val (prems, concl) = Logic.strip_horn (prop_of intro)
     7.7 -        val env = Pattern.unify thy
     7.8 +        val env = Pattern.unify (Context.Theory thy)
     7.9            (HOLogic.mk_Trueprop (list_comb (pred, pats)), concl) (Envir.empty 0)
    7.10          val prems = map (Envir.norm_term env) prems
    7.11          val args = map (Envir.norm_term env) result_pats
     8.1 --- a/src/HOL/Tools/Quotient/quotient_tacs.ML	Sat Nov 08 17:39:01 2014 +0100
     8.2 +++ b/src/HOL/Tools/Quotient/quotient_tacs.ML	Sat Nov 08 21:31:51 2014 +0100
     8.3 @@ -80,7 +80,7 @@
     8.4  
     8.5  fun get_match_inst thy pat trm =
     8.6    let
     8.7 -    val univ = Unify.matchers thy [(pat, trm)]
     8.8 +    val univ = Unify.matchers (Context.Theory thy) [(pat, trm)]
     8.9      val SOME (env, _) = Seq.pull univ           (* raises Bind, if no unifier *) (* FIXME fragile *)
    8.10      val tenv = Vartab.dest (Envir.term_env env)
    8.11      val tyenv = Vartab.dest (Envir.type_env env)
     9.1 --- a/src/HOL/Tools/TFL/casesplit.ML	Sat Nov 08 17:39:01 2014 +0100
     9.2 +++ b/src/HOL/Tools/TFL/casesplit.ML	Sat Nov 08 21:31:51 2014 +0100
     9.3 @@ -122,7 +122,7 @@
     9.4        (* check if we are a member of splitths - FIXME: quicker and
     9.5        more flexible with discrim net. *)
     9.6        fun solve_by_splitth th split =
     9.7 -        Thm.biresolution false [(false,split)] 1 th;
     9.8 +        Thm.biresolution (SOME ctxt) false [(false,split)] 1 th;
     9.9  
    9.10        fun split th =
    9.11          (case find_thms_split splitths 1 th of
    10.1 --- a/src/Provers/blast.ML	Sat Nov 08 17:39:01 2014 +0100
    10.2 +++ b/src/Provers/blast.ML	Sat Nov 08 21:31:51 2014 +0100
    10.3 @@ -461,7 +461,7 @@
    10.4  
    10.5  
    10.6  (*Like dup_elim, but puts the duplicated major premise FIRST*)
    10.7 -fun rev_dup_elim th = (th RSN (2, revcut_rl)) |> Thm.assumption 2 |> Seq.hd;
    10.8 +fun rev_dup_elim th = (th RSN (2, revcut_rl)) |> Thm.assumption NONE 2 |> Seq.hd;
    10.9  
   10.10  
   10.11  (*Rotate the assumptions in all new subgoals for the LIFO discipline*)
    11.1 --- a/src/Provers/classical.ML	Sat Nov 08 17:39:01 2014 +0100
    11.2 +++ b/src/Provers/classical.ML	Sat Nov 08 21:31:51 2014 +0100
    11.3 @@ -207,7 +207,7 @@
    11.4  
    11.5  fun dup_elim th =  (* FIXME proper context!? *)
    11.6    let
    11.7 -    val rl = (th RSN (2, revcut_rl)) |> Thm.assumption 2 |> Seq.hd;
    11.8 +    val rl = (th RSN (2, revcut_rl)) |> Thm.assumption NONE 2 |> Seq.hd;
    11.9      val ctxt = Proof_Context.init_global (Thm.theory_of_thm rl);
   11.10    in rule_by_tactic ctxt (TRYALL (eresolve_tac [revcut_rl])) rl end;
   11.11  
   11.12 @@ -906,7 +906,7 @@
   11.13      val {xtra_netpair, ...} = rep_claset_of ctxt;
   11.14      val rules3 = Context_Rules.find_rules_netpair true facts goal xtra_netpair;
   11.15      val rules = rules1 @ rules2 @ rules3 @ rules4;
   11.16 -    val ruleq = Drule.multi_resolves facts rules;
   11.17 +    val ruleq = Drule.multi_resolves (SOME ctxt) facts rules;
   11.18      val _ = Method.trace ctxt rules;
   11.19    in
   11.20      fn st => Seq.maps (fn rule => resolve_tac [rule] i st) ruleq
    12.1 --- a/src/Provers/hypsubst.ML	Sat Nov 08 17:39:01 2014 +0100
    12.2 +++ b/src/Provers/hypsubst.ML	Sat Nov 08 21:31:51 2014 +0100
    12.3 @@ -196,7 +196,7 @@
    12.4  
    12.5  val imp_intr_tac = resolve_tac [Data.imp_intr];
    12.6  
    12.7 -fun rev_dup_elim th = (th RSN (2, revcut_rl)) |> Thm.assumption 2 |> Seq.hd;
    12.8 +fun rev_dup_elim th = (th RSN (2, revcut_rl)) |> Thm.assumption NONE 2 |> Seq.hd;
    12.9  val dup_subst = rev_dup_elim ssubst
   12.10  
   12.11  (* FIXME: "etac Data.rev_mp i" will not behave as expected if goal has *)
    13.1 --- a/src/Pure/Isar/calculation.ML	Sat Nov 08 17:39:01 2014 +0100
    13.2 +++ b/src/Pure/Isar/calculation.ML	Sat Nov 08 21:31:51 2014 +0100
    13.3 @@ -85,8 +85,9 @@
    13.4  
    13.5  (* symmetric *)
    13.6  
    13.7 -val symmetric = Thm.rule_attribute (fn x => fn th =>
    13.8 -  (case Seq.chop 2 (Drule.multi_resolves [th] (#2 (#1 (Data.get x)))) of
    13.9 +val symmetric = Thm.rule_attribute (fn context => fn th =>
   13.10 +  (case Seq.chop 2
   13.11 +      (Drule.multi_resolves (SOME (Context.proof_of context)) [th] (#2 (#1 (Data.get context)))) of
   13.12      ([th'], _) => Drule.zero_var_indexes th'
   13.13    | ([], _) => raise THM ("symmetric: no unifiers", 1, [th])
   13.14    | _ => raise THM ("symmetric: multiple unifiers", 1, [th])));
   13.15 @@ -155,7 +156,7 @@
   13.16              (case ths of
   13.17                [] => Item_Net.content (#1 (get_rules ctxt))
   13.18              | th :: _ => Item_Net.retrieve (#1 (get_rules ctxt)) (strip_assums_concl th)))
   13.19 -        |> Seq.of_list |> Seq.maps (Drule.multi_resolve ths)
   13.20 +        |> Seq.of_list |> Seq.maps (Drule.multi_resolve (SOME ctxt) ths)
   13.21          |> Seq.map (check_projection ths))
   13.22          (Seq.single (Seq.Error (fn () =>
   13.23            (Pretty.string_of o Pretty.block o Pretty.fbreaks)
    14.1 --- a/src/Pure/Isar/method.ML	Sat Nov 08 17:39:01 2014 +0100
    14.2 +++ b/src/Pure/Isar/method.ML	Sat Nov 08 21:31:51 2014 +0100
    14.3 @@ -185,7 +185,7 @@
    14.4      | _ => K no_tac));
    14.5  
    14.6  fun finish immed ctxt =
    14.7 -  METHOD (K ((if immed then all_assm_tac ctxt else all_tac) THEN flexflex_tac));
    14.8 +  METHOD (K ((if immed then all_assm_tac ctxt else all_tac) THEN flexflex_tac ctxt));
    14.9  
   14.10  end;
   14.11  
   14.12 @@ -205,7 +205,9 @@
   14.13  fun gen_rule_tac tac ctxt rules facts =
   14.14    (fn i => fn st =>
   14.15      if null facts then tac rules i st
   14.16 -    else Seq.maps (fn rule => (tac o single) rule i st) (Drule.multi_resolves facts rules))
   14.17 +    else
   14.18 +      Seq.maps (fn rule => (tac o single) rule i st)
   14.19 +        (Drule.multi_resolves (SOME ctxt) facts rules))
   14.20    THEN_ALL_NEW Goal.norm_hhf_tac ctxt;
   14.21  
   14.22  fun gen_arule_tac tac ctxt j rules facts =
    15.1 --- a/src/Pure/Isar/proof.ML	Sat Nov 08 17:39:01 2014 +0100
    15.2 +++ b/src/Pure/Isar/proof.ML	Sat Nov 08 21:31:51 2014 +0100
    15.3 @@ -471,7 +471,7 @@
    15.4      val th =
    15.5        (Goal.conclude (if length (flat propss) > 1 then Thm.norm_proof goal else goal)
    15.6          handle THM _ => lost_structure ())
    15.7 -      |> Drule.flexflex_unique
    15.8 +      |> Drule.flexflex_unique (SOME ctxt)
    15.9        |> Thm.check_shyps (Variable.sorts_of ctxt)
   15.10        |> Thm.check_hyps (Context.Proof ctxt);
   15.11  
   15.12 @@ -480,8 +480,9 @@
   15.13        Conjunction.elim_balanced (length goal_propss) th
   15.14        |> map2 Conjunction.elim_balanced (map length goal_propss)
   15.15        handle THM _ => lost_structure ();
   15.16 -    val _ = Unify.matches_list thy (flat goal_propss) (map Thm.prop_of (flat results)) orelse
   15.17 -      error ("Proved a different theorem:\n" ^ Display.string_of_thm ctxt th);
   15.18 +    val _ =
   15.19 +      Unify.matches_list (Context.Proof ctxt) (flat goal_propss) (map Thm.prop_of (flat results))
   15.20 +        orelse error ("Proved a different theorem:\n" ^ Display.string_of_thm ctxt th);
   15.21  
   15.22      fun recover_result ([] :: pss) thss = [] :: recover_result pss thss
   15.23        | recover_result (_ :: pss) (ths :: thss) = ths :: recover_result pss thss
    16.1 --- a/src/Pure/Isar/proof_context.ML	Sat Nov 08 17:39:01 2014 +0100
    16.2 +++ b/src/Pure/Isar/proof_context.ML	Sat Nov 08 21:31:51 2014 +0100
    16.3 @@ -790,7 +790,7 @@
    16.4  (* simult_matches *)
    16.5  
    16.6  fun simult_matches ctxt (t, pats) =
    16.7 -  (case Seq.pull (Unify.matchers (theory_of ctxt) (map (rpair t) pats)) of
    16.8 +  (case Seq.pull (Unify.matchers (Context.Proof ctxt) (map (rpair t) pats)) of
    16.9      NONE => error "Pattern match failed!"
   16.10    | SOME (env, _) => Vartab.fold (fn (v, (_, t)) => cons (v, t)) (Envir.term_env env) []);
   16.11  
   16.12 @@ -898,17 +898,18 @@
   16.13  
   16.14  local
   16.15  
   16.16 -fun comp_hhf_tac th i st =
   16.17 -  PRIMSEQ (Thm.bicompose {flatten = true, match = false, incremented = true}
   16.18 +fun comp_hhf_tac ctxt th i st =
   16.19 +  PRIMSEQ (Thm.bicompose (SOME ctxt) {flatten = true, match = false, incremented = true}
   16.20      (false, Drule.lift_all (Thm.cprem_of st i) th, 0) i) st;
   16.21  
   16.22 -fun comp_incr_tac [] _ = no_tac
   16.23 -  | comp_incr_tac (th :: ths) i =
   16.24 -      (fn st => comp_hhf_tac (Drule.incr_indexes st th) i st) APPEND comp_incr_tac ths i;
   16.25 +fun comp_incr_tac _ [] _ = no_tac
   16.26 +  | comp_incr_tac ctxt (th :: ths) i =
   16.27 +      (fn st => comp_hhf_tac ctxt (Drule.incr_indexes st th) i st) APPEND
   16.28 +      comp_incr_tac ctxt ths i;
   16.29  
   16.30  in
   16.31  
   16.32 -fun fact_tac ctxt facts = Goal.norm_hhf_tac ctxt THEN' comp_incr_tac facts;
   16.33 +fun fact_tac ctxt facts = Goal.norm_hhf_tac ctxt THEN' comp_incr_tac ctxt facts;
   16.34  
   16.35  fun potential_facts ctxt prop =
   16.36    Facts.could_unify (facts_of ctxt) (Term.strip_all_body prop);
    17.1 --- a/src/Pure/Isar/rule_cases.ML	Sat Nov 08 17:39:01 2014 +0100
    17.2 +++ b/src/Pure/Isar/rule_cases.ML	Sat Nov 08 21:31:51 2014 +0100
    17.3 @@ -221,7 +221,7 @@
    17.4      th
    17.5      |> unfold_prems ctxt n defs
    17.6      |> unfold_prems_concls ctxt defs
    17.7 -    |> Drule.multi_resolve (take m facts)
    17.8 +    |> Drule.multi_resolve (SOME ctxt) (take m facts)
    17.9      |> Seq.map (pair (xx, (n - m, drop m facts)))
   17.10    end;
   17.11  
    18.1 --- a/src/Pure/Proof/extraction.ML	Sat Nov 08 17:39:01 2014 +0100
    18.2 +++ b/src/Pure/Proof/extraction.ML	Sat Nov 08 21:31:51 2014 +0100
    18.3 @@ -107,7 +107,7 @@
    18.4            val env' = Envir.Envir
    18.5              {maxidx = fold (fn (t, u) => Term.maxidx_term t #> Term.maxidx_term u) prems' ~1,
    18.6               tenv = tenv, tyenv = Tenv};
    18.7 -          val env'' = fold (Pattern.unify thy o pairself (lookup rew)) prems' env';
    18.8 +          val env'' = fold (Pattern.unify (Context.Theory thy) o pairself (lookup rew)) prems' env';
    18.9          in SOME (Envir.norm_term env'' (inc (ren tm2)))
   18.10          end handle Pattern.MATCH => NONE | Pattern.Unif => NONE)
   18.11            (sort (int_ord o pairself fst)
    19.1 --- a/src/Pure/Proof/reconstruct.ML	Sat Nov 08 17:39:01 2014 +0100
    19.2 +++ b/src/Pure/Proof/reconstruct.ML	Sat Nov 08 21:31:51 2014 +0100
    19.3 @@ -121,7 +121,7 @@
    19.4          val t' = mk_abs Ts t;
    19.5          val u' = mk_abs Ts u
    19.6        in
    19.7 -        (prop, prf, cs, Pattern.unify thy (t', u') env, vTs)
    19.8 +        (prop, prf, cs, Pattern.unify (Context.Theory thy) (t', u') env, vTs)
    19.9          handle Pattern.Pattern =>
   19.10              let val (cs', env') = decompose thy [] (t', u') env
   19.11              in (prop, prf, cs @ cs', env', vTs) end
   19.12 @@ -263,7 +263,7 @@
   19.13                    val tn2 = Envir.norm_term bigenv t2
   19.14                  in
   19.15                    if Pattern.pattern tn1 andalso Pattern.pattern tn2 then
   19.16 -                    (Pattern.unify thy (tn1, tn2) env, ps) handle Pattern.Unif =>
   19.17 +                    (Pattern.unify (Context.Theory thy) (tn1, tn2) env, ps) handle Pattern.Unif =>
   19.18                         cantunify thy (tn1, tn2)
   19.19                    else
   19.20                      let val (cs', env') = decompose thy [] (tn1, tn2) env
    20.1 --- a/src/Pure/Tools/rule_insts.ML	Sat Nov 08 17:39:01 2014 +0100
    20.2 +++ b/src/Pure/Tools/rule_insts.ML	Sat Nov 08 21:31:51 2014 +0100
    20.3 @@ -24,7 +24,7 @@
    20.4      (binding * string option * mixfix) list -> thm -> thm
    20.5    val read_instantiate: Proof.context -> (indexname * string) list -> string list -> thm -> thm
    20.6    val instantiate_tac: Proof.context -> (indexname * string) list -> string list -> tactic
    20.7 -  val make_elim_preserve: thm -> thm
    20.8 +  val make_elim_preserve: Proof.context -> thm -> thm
    20.9    val method: (Proof.context -> (indexname * string) list -> thm -> int -> tactic) ->
   20.10      (Proof.context -> thm list -> int -> tactic) -> (Proof.context -> Proof.method) context_parser
   20.11  end;
   20.12 @@ -280,7 +280,7 @@
   20.13  
   20.14  (* forward resolution *)
   20.15  
   20.16 -fun make_elim_preserve rl =
   20.17 +fun make_elim_preserve ctxt rl =
   20.18    let
   20.19      val cert = Thm.cterm_of (Thm.theory_of_thm rl);
   20.20      val maxidx = Thm.maxidx_of rl;
   20.21 @@ -290,7 +290,7 @@
   20.22          (cvar ("W", 0), cvar ("W", maxidx + 1))]) Drule.revcut_rl;
   20.23    in
   20.24      (case Seq.list_of
   20.25 -      (Thm.bicompose {flatten = true, match = false, incremented = false}
   20.26 +      (Thm.bicompose (SOME ctxt) {flatten = true, match = false, incremented = false}
   20.27          (false, rl, Thm.nprems_of rl) 1 revcut_rl')
   20.28       of
   20.29        [th] => th
   20.30 @@ -298,13 +298,13 @@
   20.31    end;
   20.32  
   20.33  (*instantiate and cut -- for atomic fact*)
   20.34 -fun cut_inst_tac ctxt insts rule = res_inst_tac ctxt insts (make_elim_preserve rule);
   20.35 +fun cut_inst_tac ctxt insts rule = res_inst_tac ctxt insts (make_elim_preserve ctxt rule);
   20.36  
   20.37  (*forward tactic applies a rule to an assumption without deleting it*)
   20.38  fun forw_inst_tac ctxt insts rule = cut_inst_tac ctxt insts rule THEN' assume_tac;
   20.39  
   20.40  (*dresolve tactic applies a rule to replace an assumption*)
   20.41 -fun dres_inst_tac ctxt insts rule = eres_inst_tac ctxt insts (make_elim_preserve rule);
   20.42 +fun dres_inst_tac ctxt insts rule = eres_inst_tac ctxt insts (make_elim_preserve ctxt rule);
   20.43  
   20.44  
   20.45  (* derived tactics *)
    21.1 --- a/src/Pure/drule.ML	Sat Nov 08 17:39:01 2014 +0100
    21.2 +++ b/src/Pure/drule.ML	Sat Nov 08 21:31:51 2014 +0100
    21.3 @@ -59,15 +59,15 @@
    21.4    val strip_type: ctyp -> ctyp list * ctyp
    21.5    val beta_conv: cterm -> cterm -> cterm
    21.6    val types_sorts: thm -> (indexname-> typ option) * (indexname-> sort option)
    21.7 -  val flexflex_unique: thm -> thm
    21.8 +  val flexflex_unique: Proof.context option -> thm -> thm
    21.9    val export_without_context: thm -> thm
   21.10    val export_without_context_open: thm -> thm
   21.11    val store_thm: binding -> thm -> thm
   21.12    val store_standard_thm: binding -> thm -> thm
   21.13    val store_thm_open: binding -> thm -> thm
   21.14    val store_standard_thm_open: binding -> thm -> thm
   21.15 -  val multi_resolve: thm list -> thm -> thm Seq.seq
   21.16 -  val multi_resolves: thm list -> thm list -> thm Seq.seq
   21.17 +  val multi_resolve: Proof.context option -> thm list -> thm -> thm Seq.seq
   21.18 +  val multi_resolves: Proof.context option -> thm list -> thm list -> thm Seq.seq
   21.19    val compose: thm * int * thm -> thm
   21.20    val equals_cong: thm
   21.21    val imp_cong: thm
   21.22 @@ -268,9 +268,9 @@
   21.23  
   21.24  (*Squash a theorem's flexflex constraints provided it can be done uniquely.
   21.25    This step can lose information.*)
   21.26 -fun flexflex_unique th =
   21.27 +fun flexflex_unique opt_ctxt th =
   21.28    if null (Thm.tpairs_of th) then th else
   21.29 -    case distinct Thm.eq_thm (Seq.list_of (Thm.flexflex_rule th)) of
   21.30 +    case distinct Thm.eq_thm (Seq.list_of (Thm.flexflex_rule opt_ctxt th)) of
   21.31        [th] => th
   21.32      | []   => raise THM("flexflex_unique: impossible constraints", 0, [th])
   21.33      |  _   => raise THM("flexflex_unique: multiple unifiers", 0, [th]);
   21.34 @@ -289,7 +289,7 @@
   21.35      #> Thm.varifyT_global);
   21.36  
   21.37  val export_without_context =
   21.38 -  flexflex_unique
   21.39 +  flexflex_unique NONE
   21.40    #> export_without_context_open
   21.41    #> Thm.close_derivation;
   21.42  
   21.43 @@ -315,19 +315,21 @@
   21.44  
   21.45  (*Resolution: multiple arguments, multiple results*)
   21.46  local
   21.47 -  fun res th i rule =
   21.48 -    Thm.biresolution false [(false, th)] i rule handle THM _ => Seq.empty;
   21.49 +  fun res opt_ctxt th i rule =
   21.50 +    Thm.biresolution opt_ctxt false [(false, th)] i rule handle THM _ => Seq.empty;
   21.51  
   21.52 -  fun multi_res _ [] rule = Seq.single rule
   21.53 -    | multi_res i (th :: ths) rule = Seq.maps (res th i) (multi_res (i + 1) ths rule);
   21.54 +  fun multi_res _ _ [] rule = Seq.single rule
   21.55 +    | multi_res opt_ctxt i (th :: ths) rule =
   21.56 +        Seq.maps (res opt_ctxt th i) (multi_res opt_ctxt (i + 1) ths rule);
   21.57  in
   21.58 -  val multi_resolve = multi_res 1;
   21.59 -  fun multi_resolves facts rules = Seq.maps (multi_resolve facts) (Seq.of_list rules);
   21.60 +  fun multi_resolve opt_ctxt = multi_res opt_ctxt 1;
   21.61 +  fun multi_resolves opt_ctxt facts rules =
   21.62 +    Seq.maps (multi_resolve opt_ctxt facts) (Seq.of_list rules);
   21.63  end;
   21.64  
   21.65  (*Resolution: exactly one resolvent must be produced*)
   21.66  fun tha RSN (i, thb) =
   21.67 -  (case Seq.chop 2 (Thm.biresolution false [(false, tha)] i thb) of
   21.68 +  (case Seq.chop 2 (Thm.biresolution NONE false [(false, tha)] i thb) of
   21.69      ([th], _) => th
   21.70    | ([], _) => raise THM ("RSN: no unifiers", i, [tha, thb])
   21.71    | _ => raise THM ("RSN: multiple unifiers", i, [tha, thb]));
   21.72 @@ -337,7 +339,7 @@
   21.73  
   21.74  (*For joining lists of rules*)
   21.75  fun thas RLN (i, thbs) =
   21.76 -  let val resolve = Thm.biresolution false (map (pair false) thas) i
   21.77 +  let val resolve = Thm.biresolution NONE false (map (pair false) thas) i
   21.78        fun resb thb = Seq.list_of (resolve thb) handle THM _ => []
   21.79    in maps resb thbs end;
   21.80  
   21.81 @@ -345,7 +347,7 @@
   21.82  
   21.83  (*Isar-style multi-resolution*)
   21.84  fun bottom_rl OF rls =
   21.85 -  (case Seq.chop 2 (multi_resolve rls bottom_rl) of
   21.86 +  (case Seq.chop 2 (multi_resolve NONE rls bottom_rl) of
   21.87      ([th], _) => th
   21.88    | ([], _) => raise THM ("OF: no unifiers", 0, bottom_rl :: rls)
   21.89    | _ => raise THM ("OF: multiple unifiers", 0, bottom_rl :: rls));
   21.90 @@ -358,7 +360,7 @@
   21.91    with no lifting or renaming!  Q may contain ==> or meta-quants
   21.92    ALWAYS deletes premise i *)
   21.93  fun compose (tha, i, thb) =
   21.94 -  Thm.bicompose {flatten = true, match = false, incremented = false} (false, tha, 0) i thb
   21.95 +  Thm.bicompose NONE {flatten = true, match = false, incremented = false} (false, tha, 0) i thb
   21.96    |> Seq.list_of |> distinct Thm.eq_thm
   21.97    |> (fn [th] => th | _ => raise THM ("compose: unique result expected", i, [tha, thb]));
   21.98  
   21.99 @@ -739,7 +741,7 @@
  21.100  
  21.101  (*compose Q and [Q1,Q2,...,Qk]==>R to [Q2,...,Qk]==>R getting unique result*)
  21.102  fun comp incremented th1 th2 =
  21.103 -  Thm.bicompose {flatten = true, match = false, incremented = incremented} (false, th1, 0) 1 th2
  21.104 +  Thm.bicompose NONE {flatten = true, match = false, incremented = incremented} (false, th1, 0) 1 th2
  21.105    |> Seq.list_of |> distinct Thm.eq_thm
  21.106    |> (fn [th] => th | _ => raise THM ("COMP", 1, [th1, th2]));
  21.107  
  21.108 @@ -753,7 +755,7 @@
  21.109  
  21.110  fun comp_no_flatten (th, n) i rule =
  21.111    (case distinct Thm.eq_thm (Seq.list_of
  21.112 -      (Thm.bicompose {flatten = false, match = false, incremented = true}
  21.113 +      (Thm.bicompose NONE {flatten = false, match = false, incremented = true}
  21.114          (false, th, n) i (incr_indexes th rule))) of
  21.115      [th'] => th'
  21.116    | [] => raise THM ("comp_no_flatten", i, [th, rule])
    22.1 --- a/src/Pure/goal.ML	Sat Nov 08 17:39:01 2014 +0100
    22.2 +++ b/src/Pure/goal.ML	Sat Nov 08 21:31:51 2014 +0100
    22.3 @@ -97,7 +97,7 @@
    22.4  (* normal form *)
    22.5  
    22.6  fun norm_result ctxt =
    22.7 -  Drule.flexflex_unique
    22.8 +  Drule.flexflex_unique (SOME ctxt)
    22.9    #> Raw_Simplifier.norm_hhf_protect ctxt
   22.10    #> Thm.strip_shyps
   22.11    #> Drule.zero_var_indexes;
   22.12 @@ -144,7 +144,7 @@
   22.13        cert (Logic.varify_types_global (fold_rev Logic.all xs (Logic.list_implies (As, prop))))
   22.14        |> Thm.weaken_sorts (Variable.sorts_of ctxt);
   22.15      val global_result = result |> Future.map
   22.16 -      (Drule.flexflex_unique #>
   22.17 +      (Drule.flexflex_unique (SOME ctxt) #>
   22.18          Thm.adjust_maxidx_thm ~1 #>
   22.19          Drule.implies_intr_list assms #>
   22.20          Drule.forall_intr_list fixes #>
   22.21 @@ -216,12 +216,13 @@
   22.22                Theory.subthy (theory_of_thm st, thy) orelse err "Bad background theory of goal state";
   22.23              val res =
   22.24                (finish ctxt' st
   22.25 -                |> Drule.flexflex_unique
   22.26 +                |> Drule.flexflex_unique (SOME ctxt')
   22.27                  |> Thm.check_shyps sorts
   22.28                  |> Thm.check_hyps (Context.Proof ctxt'))
   22.29                handle THM (msg, _, _) => err msg | ERROR msg => err msg;
   22.30            in
   22.31 -            if Unify.matches_list thy [Thm.term_of stmt] [Thm.prop_of res] then res
   22.32 +            if Unify.matches_list (Context.Proof ctxt') [Thm.term_of stmt] [Thm.prop_of res]
   22.33 +            then res
   22.34              else err ("Proved a different theorem: " ^ Syntax.string_of_term ctxt' (Thm.prop_of res))
   22.35            end);
   22.36      val res =
    23.1 --- a/src/Pure/par_tactical.ML	Sat Nov 08 17:39:01 2014 +0100
    23.2 +++ b/src/Pure/par_tactical.ML	Sat Nov 08 21:31:51 2014 +0100
    23.3 @@ -35,7 +35,7 @@
    23.4  
    23.5  fun retrofit st' =
    23.6    rotate_prems ~1 #>
    23.7 -  Thm.bicompose {flatten = false, match = false, incremented = false}
    23.8 +  Thm.bicompose NONE {flatten = false, match = false, incremented = false}
    23.9        (false, Goal.conclude st', Thm.nprems_of st') 1;
   23.10  
   23.11  in
    24.1 --- a/src/Pure/pattern.ML	Sat Nov 08 17:39:01 2014 +0100
    24.2 +++ b/src/Pure/pattern.ML	Sat Nov 08 21:31:51 2014 +0100
    24.3 @@ -12,8 +12,13 @@
    24.4  
    24.5  signature PATTERN =
    24.6  sig
    24.7 +  exception Unif
    24.8 +  exception Pattern
    24.9    val unify_trace_failure_raw: Config.raw
   24.10    val unify_trace_failure: bool Config.T
   24.11 +  val unify_types: Context.generic -> typ * typ -> Envir.env -> Envir.env
   24.12 +  val unify: Context.generic -> term * term -> Envir.env -> Envir.env
   24.13 +  exception MATCH
   24.14    val match: theory -> term * term -> Type.tyenv * Envir.tenv -> Type.tyenv * Envir.tenv
   24.15    val first_order_match: theory -> term * term
   24.16      -> Type.tyenv * Envir.tenv -> Type.tyenv * Envir.tenv
   24.17 @@ -21,16 +26,11 @@
   24.18    val matchess: theory -> term list * term list -> bool
   24.19    val equiv: theory -> term * term -> bool
   24.20    val matches_subterm: theory -> term * term -> bool
   24.21 -  val unify_types: theory -> typ * typ -> Envir.env -> Envir.env
   24.22 -  val unify: theory -> term * term -> Envir.env -> Envir.env
   24.23    val first_order: term -> bool
   24.24    val pattern: term -> bool
   24.25    val match_rew: theory -> term -> term * term -> (term * term) option
   24.26    val rewrite_term: theory -> (term * term) list -> (term -> term option) list -> term -> term
   24.27    val rewrite_term_top: theory -> (term * term) list -> (term -> term option) list -> term -> term
   24.28 -  exception Unif
   24.29 -  exception MATCH
   24.30 -  exception Pattern
   24.31  end;
   24.32  
   24.33  structure Pattern: PATTERN =
   24.34 @@ -40,59 +40,62 @@
   24.35  exception Pattern;
   24.36  
   24.37  val unify_trace_failure_raw =
   24.38 -  Config.declare_global ("unify_trace_failure", @{here}) (fn _ => Config.Bool false);
   24.39 +  Config.declare ("unify_trace_failure", @{here}) (fn _ => Config.Bool false);
   24.40  val unify_trace_failure = Config.bool unify_trace_failure_raw;
   24.41  
   24.42 -fun string_of_term thy env binders t =
   24.43 -  Syntax.string_of_term_global thy
   24.44 -    (Envir.norm_term env (subst_bounds (map Free binders, t)));
   24.45 +fun string_of_term ctxt env binders t =
   24.46 +  Syntax.string_of_term ctxt (Envir.norm_term env (subst_bounds (map Free binders, t)));
   24.47  
   24.48  fun bname binders i = fst (nth binders i);
   24.49  fun bnames binders is = space_implode " " (map (bname binders) is);
   24.50  
   24.51 -fun typ_clash thy (tye,T,U) =
   24.52 -  if Config.get_global thy unify_trace_failure
   24.53 -  then let val t = Syntax.string_of_typ_global thy (Envir.norm_type tye T)
   24.54 -           and u = Syntax.string_of_typ_global thy (Envir.norm_type tye U)
   24.55 -       in tracing("The following types do not unify:\n" ^ t ^ "\n" ^ u) end
   24.56 -  else ()
   24.57 +fun typ_clash context (tye,T,U) =
   24.58 +  if Config.get_generic context unify_trace_failure then
   24.59 +    let
   24.60 +      val ctxt = Context.proof_of context;
   24.61 +      val t = Syntax.string_of_typ ctxt (Envir.norm_type tye T);
   24.62 +      val u = Syntax.string_of_typ ctxt (Envir.norm_type tye U);
   24.63 +    in tracing ("The following types do not unify:\n" ^ t ^ "\n" ^ u) end
   24.64 +  else ();
   24.65  
   24.66 -fun clash thy a b =
   24.67 -  if Config.get_global thy unify_trace_failure then tracing("Clash: " ^ a ^ " =/= " ^ b) else ()
   24.68 +fun clash context a b =
   24.69 +  if Config.get_generic context unify_trace_failure
   24.70 +  then tracing ("Clash: " ^ a ^ " =/= " ^ b) else ();
   24.71  
   24.72  fun boundVar binders i =
   24.73    "bound variable " ^ bname binders i ^ " (depth " ^ string_of_int i ^ ")";
   24.74  
   24.75 -fun clashBB thy binders i j =
   24.76 -  if Config.get_global thy unify_trace_failure
   24.77 -  then clash thy (boundVar binders i) (boundVar binders j)
   24.78 -  else ()
   24.79 +fun clashBB context binders i j =
   24.80 +  if Config.get_generic context unify_trace_failure
   24.81 +  then clash context (boundVar binders i) (boundVar binders j) else ();
   24.82  
   24.83 -fun clashB thy binders i s =
   24.84 -  if Config.get_global thy unify_trace_failure
   24.85 -  then clash thy (boundVar binders i) s
   24.86 -  else ()
   24.87 +fun clashB context binders i s =
   24.88 +  if Config.get_generic context unify_trace_failure
   24.89 +  then clash context (boundVar binders i) s else ();
   24.90  
   24.91 -fun proj_fail thy (env,binders,F,_,is,t) =
   24.92 -  if Config.get_global thy unify_trace_failure
   24.93 -  then let val f = Term.string_of_vname F
   24.94 -           val xs = bnames binders is
   24.95 -           val u = string_of_term thy env binders t
   24.96 -           val ys = bnames binders (subtract (op =) is (loose_bnos t))
   24.97 -       in tracing("Cannot unify variable " ^ f ^
   24.98 -               " (depending on bound variables " ^ xs ^ ")\nwith term " ^ u ^
   24.99 -               "\nTerm contains additional bound variable(s) " ^ ys)
  24.100 -       end
  24.101 -  else ()
  24.102 +fun proj_fail context (env,binders,F,_,is,t) =
  24.103 +  if Config.get_generic context unify_trace_failure then
  24.104 +    let
  24.105 +      val ctxt = Context.proof_of context
  24.106 +      val f = Term.string_of_vname F
  24.107 +      val xs = bnames binders is
  24.108 +      val u = string_of_term ctxt env binders t
  24.109 +      val ys = bnames binders (subtract (op =) is (loose_bnos t))
  24.110 +    in
  24.111 +      tracing ("Cannot unify variable " ^ f ^
  24.112 +        " (depending on bound variables " ^ xs ^ ")\nwith term " ^ u ^
  24.113 +        "\nTerm contains additional bound variable(s) " ^ ys)
  24.114 +    end
  24.115 +  else ();
  24.116  
  24.117 -fun ocheck_fail thy (F,t,binders,env) =
  24.118 -  if Config.get_global thy unify_trace_failure
  24.119 -  then let val f = Term.string_of_vname F
  24.120 -           val u = string_of_term thy env binders t
  24.121 -       in tracing("Variable " ^ f ^ " occurs in term\n" ^ u ^
  24.122 -                  "\nCannot unify!\n")
  24.123 -       end
  24.124 -  else ()
  24.125 +fun ocheck_fail context (F,t,binders,env) =
  24.126 +  if Config.get_generic context unify_trace_failure then
  24.127 +    let
  24.128 +      val ctxt = Context.proof_of context
  24.129 +      val f = Term.string_of_vname F
  24.130 +      val u = string_of_term ctxt env binders t
  24.131 +    in tracing ("Variable " ^ f ^ " occurs in term\n" ^ u ^ "\nCannot unify!\n") end
  24.132 +  else ();
  24.133  
  24.134  fun occurs(F,t,env) =
  24.135      let fun occ(Var (G, T))   = (case Envir.lookup env (G, T) of
  24.136 @@ -230,55 +233,57 @@
  24.137                   end;
  24.138    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
  24.139  
  24.140 -fun unify_types thy (T, U) (env as Envir.Envir {maxidx, tenv, tyenv}) =
  24.141 +fun unify_types context (T, U) (env as Envir.Envir {maxidx, tenv, tyenv}) =
  24.142    if T = U then env
  24.143    else
  24.144 -    let val (tyenv', maxidx') = Sign.typ_unify thy (U, T) (tyenv, maxidx)
  24.145 +    let
  24.146 +      val thy = Context.theory_of context
  24.147 +      val (tyenv', maxidx') = Sign.typ_unify thy (U, T) (tyenv, maxidx)
  24.148      in Envir.Envir {maxidx = maxidx', tenv = tenv, tyenv = tyenv'} end
  24.149 -    handle Type.TUNIFY => (typ_clash thy (tyenv, T, U); raise Unif);
  24.150 +    handle Type.TUNIFY => (typ_clash context (tyenv, T, U); raise Unif);
  24.151  
  24.152 -fun unif thy binders (s,t) env = case (Envir.head_norm env s, Envir.head_norm env t) of
  24.153 +fun unif context binders (s,t) env = case (Envir.head_norm env s, Envir.head_norm env t) of
  24.154        (Abs(ns,Ts,ts),Abs(nt,Tt,tt)) =>
  24.155           let val name = if ns = "" then nt else ns
  24.156 -         in unif thy ((name,Ts)::binders) (ts,tt) (unify_types thy (Ts, Tt) env) end
  24.157 -    | (Abs(ns,Ts,ts),t) => unif thy ((ns,Ts)::binders) (ts,(incr t)$Bound(0)) env
  24.158 -    | (t,Abs(nt,Tt,tt)) => unif thy ((nt,Tt)::binders) ((incr t)$Bound(0),tt) env
  24.159 -    | p => cases thy (binders,env,p)
  24.160 +         in unif context ((name,Ts)::binders) (ts,tt) (unify_types context (Ts, Tt) env) end
  24.161 +    | (Abs(ns,Ts,ts),t) => unif context ((ns,Ts)::binders) (ts,(incr t)$Bound(0)) env
  24.162 +    | (t,Abs(nt,Tt,tt)) => unif context ((nt,Tt)::binders) ((incr t)$Bound(0),tt) env
  24.163 +    | p => cases context (binders,env,p)
  24.164  
  24.165 -and cases thy (binders,env,(s,t)) = case (strip_comb s,strip_comb t) of
  24.166 +and cases context (binders,env,(s,t)) = case (strip_comb s,strip_comb t) of
  24.167         ((Var(F,Fty),ss),(Var(G,Gty),ts)) =>
  24.168           if F = G then flexflex1(env,binders,F,Fty,ints_of' env ss,ints_of' env ts)
  24.169                    else flexflex2(env,binders,F,Fty,ints_of' env ss,G,Gty,ints_of' env ts)
  24.170 -      | ((Var(F,Fty),ss),_)           => flexrigid thy (env,binders,F,Fty,ints_of' env ss,t)
  24.171 -      | (_,(Var(F,Fty),ts))           => flexrigid thy (env,binders,F,Fty,ints_of' env ts,s)
  24.172 -      | ((Const c,ss),(Const d,ts))   => rigidrigid thy (env,binders,c,d,ss,ts)
  24.173 -      | ((Free(f),ss),(Free(g),ts))   => rigidrigid thy (env,binders,f,g,ss,ts)
  24.174 -      | ((Bound(i),ss),(Bound(j),ts)) => rigidrigidB thy (env,binders,i,j,ss,ts)
  24.175 +      | ((Var(F,Fty),ss),_)           => flexrigid context (env,binders,F,Fty,ints_of' env ss,t)
  24.176 +      | (_,(Var(F,Fty),ts))           => flexrigid context (env,binders,F,Fty,ints_of' env ts,s)
  24.177 +      | ((Const c,ss),(Const d,ts))   => rigidrigid context (env,binders,c,d,ss,ts)
  24.178 +      | ((Free(f),ss),(Free(g),ts))   => rigidrigid context (env,binders,f,g,ss,ts)
  24.179 +      | ((Bound(i),ss),(Bound(j),ts)) => rigidrigidB context (env,binders,i,j,ss,ts)
  24.180        | ((Abs(_),_),_)                => raise Pattern
  24.181        | (_,(Abs(_),_))                => raise Pattern
  24.182 -      | ((Const(c,_),_),(Free(f,_),_)) => (clash thy c f; raise Unif)
  24.183 -      | ((Const(c,_),_),(Bound i,_))   => (clashB thy binders i c; raise Unif)
  24.184 -      | ((Free(f,_),_),(Const(c,_),_)) => (clash thy f c; raise Unif)
  24.185 -      | ((Free(f,_),_),(Bound i,_))    => (clashB thy binders i f; raise Unif)
  24.186 -      | ((Bound i,_),(Const(c,_),_))   => (clashB thy binders i c; raise Unif)
  24.187 -      | ((Bound i,_),(Free(f,_),_))    => (clashB thy binders i f; raise Unif)
  24.188 +      | ((Const(c,_),_),(Free(f,_),_)) => (clash context c f; raise Unif)
  24.189 +      | ((Const(c,_),_),(Bound i,_))   => (clashB context binders i c; raise Unif)
  24.190 +      | ((Free(f,_),_),(Const(c,_),_)) => (clash context f c; raise Unif)
  24.191 +      | ((Free(f,_),_),(Bound i,_))    => (clashB context binders i f; raise Unif)
  24.192 +      | ((Bound i,_),(Const(c,_),_))   => (clashB context binders i c; raise Unif)
  24.193 +      | ((Bound i,_),(Free(f,_),_))    => (clashB context binders i f; raise Unif)
  24.194  
  24.195  
  24.196 -and rigidrigid thy (env,binders,(a,Ta),(b,Tb),ss,ts) =
  24.197 -      if a<>b then (clash thy a b; raise Unif)
  24.198 -      else env |> unify_types thy (Ta,Tb) |> fold (unif thy binders) (ss~~ts)
  24.199 +and rigidrigid context (env,binders,(a,Ta),(b,Tb),ss,ts) =
  24.200 +      if a<>b then (clash context a b; raise Unif)
  24.201 +      else env |> unify_types context (Ta,Tb) |> fold (unif context binders) (ss~~ts)
  24.202  
  24.203 -and rigidrigidB thy (env,binders,i,j,ss,ts) =
  24.204 -     if i <> j then (clashBB thy binders i j; raise Unif)
  24.205 -     else fold (unif thy binders) (ss~~ts) env
  24.206 +and rigidrigidB context (env,binders,i,j,ss,ts) =
  24.207 +     if i <> j then (clashBB context binders i j; raise Unif)
  24.208 +     else fold (unif context binders) (ss~~ts) env
  24.209  
  24.210 -and flexrigid thy (params as (env,binders,F,Fty,is,t)) =
  24.211 -      if occurs(F,t,env) then (ocheck_fail thy (F,t,binders,env); raise Unif)
  24.212 +and flexrigid context (params as (env,binders,F,Fty,is,t)) =
  24.213 +      if occurs(F,t,env) then (ocheck_fail context (F,t,binders,env); raise Unif)
  24.214        else (let val (u,env') = proj(t,env,binders,is)
  24.215              in Envir.update ((F, Fty), mkabs (binders, is, u)) env' end
  24.216 -            handle Unif => (proj_fail thy params; raise Unif));
  24.217 +            handle Unif => (proj_fail context params; raise Unif));
  24.218  
  24.219 -fun unify thy = unif thy [];
  24.220 +fun unify context = unif context [];
  24.221  
  24.222  
  24.223  
    25.1 --- a/src/Pure/raw_simplifier.ML	Sat Nov 08 17:39:01 2014 +0100
    25.2 +++ b/src/Pure/raw_simplifier.ML	Sat Nov 08 21:31:51 2014 +0100
    25.3 @@ -1306,7 +1306,7 @@
    25.4      val _ =
    25.5        cond_tracing ctxt (fn () =>
    25.6          print_term ctxt "SIMPLIFIER INVOKED ON THE FOLLOWING TERM:" (term_of ct));
    25.7 -  in bottomc (mode, Option.map Drule.flexflex_unique oo prover, maxidx) ctxt ct end;
    25.8 +  in bottomc (mode, Option.map (Drule.flexflex_unique (SOME ctxt)) oo prover, maxidx) ctxt ct end;
    25.9  
   25.10  val simple_prover =
   25.11    SINGLE o (fn ctxt => ALLGOALS (resolve_tac (prems_of ctxt)));
    26.1 --- a/src/Pure/subgoal.ML	Sat Nov 08 17:39:01 2014 +0100
    26.2 +++ b/src/Pure/subgoal.ML	Sat Nov 08 21:31:51 2014 +0100
    26.3 @@ -126,7 +126,7 @@
    26.4        |> Thm.adjust_maxidx_thm idx
    26.5        |> singleton (Variable.export ctxt2 ctxt0);
    26.6    in
    26.7 -    Thm.bicompose {flatten = true, match = false, incremented = false}
    26.8 +    Thm.bicompose (SOME ctxt0) {flatten = true, match = false, incremented = false}
    26.9        (false, result, Thm.nprems_of st1) i st0
   26.10    end;
   26.11  
    27.1 --- a/src/Pure/tactic.ML	Sat Nov 08 17:39:01 2014 +0100
    27.2 +++ b/src/Pure/tactic.ML	Sat Nov 08 21:31:51 2014 +0100
    27.3 @@ -28,7 +28,7 @@
    27.4    val match_tac: thm list -> int -> tactic
    27.5    val ematch_tac: thm list -> int -> tactic
    27.6    val dmatch_tac: thm list -> int -> tactic
    27.7 -  val flexflex_tac: tactic
    27.8 +  val flexflex_tac: Proof.context -> tactic
    27.9    val distinct_subgoal_tac: int -> tactic
   27.10    val distinct_subgoals_tac: tactic
   27.11    val cut_tac: thm -> int -> tactic
   27.12 @@ -101,7 +101,7 @@
   27.13       thus (REPEAT (resolve_tac rules i)) stops once subgoal i disappears. *)
   27.14  
   27.15  (*Solve subgoal i by assumption*)
   27.16 -fun assume_tac i = PRIMSEQ (Thm.assumption i);
   27.17 +fun assume_tac i = PRIMSEQ (Thm.assumption NONE i);
   27.18  
   27.19  (*Solve subgoal i by assumption, using no unification*)
   27.20  fun eq_assume_tac i = PRIMITIVE (Thm.eq_assumption i);
   27.21 @@ -112,14 +112,14 @@
   27.22  (*The composition rule/state: no lifting or var renaming.
   27.23    The arg = (bires_flg, orule, m);  see Thm.bicompose for explanation.*)
   27.24  fun compose_tac arg i =
   27.25 -  PRIMSEQ (Thm.bicompose {flatten = true, match = false, incremented = false} arg i);
   27.26 +  PRIMSEQ (Thm.bicompose NONE {flatten = true, match = false, incremented = false} arg i);
   27.27  
   27.28  (*Converts a "destruct" rule like P&Q==>P to an "elimination" rule
   27.29    like [| P&Q; P==>R |] ==> R *)
   27.30  fun make_elim rl = zero_var_indexes (rl RS revcut_rl);
   27.31  
   27.32  (*Attack subgoal i by resolution, using flags to indicate elimination rules*)
   27.33 -fun biresolve_tac brules i = PRIMSEQ (Thm.biresolution false brules i);
   27.34 +fun biresolve_tac brules i = PRIMSEQ (Thm.biresolution NONE false brules i);
   27.35  
   27.36  (*Resolution: the simple case, works for introduction rules*)
   27.37  fun resolve_tac rules = biresolve_tac (map (pair false) rules);
   27.38 @@ -146,13 +146,13 @@
   27.39  fun solve_tac rules = resolve_tac rules THEN_ALL_NEW assume_tac;
   27.40  
   27.41  (*Matching tactics -- as above, but forbid updating of state*)
   27.42 -fun bimatch_tac brules i = PRIMSEQ (Thm.biresolution true brules i);
   27.43 +fun bimatch_tac brules i = PRIMSEQ (Thm.biresolution NONE true brules i);
   27.44  fun match_tac rules  = bimatch_tac (map (pair false) rules);
   27.45  fun ematch_tac rules = bimatch_tac (map (pair true) rules);
   27.46  fun dmatch_tac rls   = ematch_tac (map make_elim rls);
   27.47  
   27.48  (*Smash all flex-flex disagreement pairs in the proof state.*)
   27.49 -val flexflex_tac = PRIMSEQ Thm.flexflex_rule;
   27.50 +fun flexflex_tac ctxt = PRIMSEQ (Thm.flexflex_rule (SOME ctxt));
   27.51  
   27.52  (*Remove duplicate subgoals.*)
   27.53  val permute_tac = PRIMITIVE oo Thm.permute_prems;
   27.54 @@ -244,7 +244,7 @@
   27.55        let val hyps = Logic.strip_assums_hyp prem
   27.56            and concl = Logic.strip_assums_concl prem
   27.57            val kbrls = Net.unify_term inet concl @ maps (Net.unify_term enet) hyps
   27.58 -      in PRIMSEQ (Thm.biresolution match (order kbrls) i) end);
   27.59 +      in PRIMSEQ (Thm.biresolution NONE match (order kbrls) i) end);
   27.60  
   27.61  (*versions taking pre-built nets.  No filtering of brls*)
   27.62  val biresolve_from_nets_tac = biresolution_from_nets_tac order_list false;
   27.63 @@ -269,15 +269,12 @@
   27.64  
   27.65  (*resolution using a net rather than rules; pred supports filt_resolve_tac*)
   27.66  fun filt_resolution_from_net_tac match pred net =
   27.67 -  SUBGOAL
   27.68 -    (fn (prem,i) =>
   27.69 -      let val krls = Net.unify_term net (Logic.strip_assums_concl prem)
   27.70 -      in
   27.71 -         if pred krls
   27.72 -         then PRIMSEQ
   27.73 -                (Thm.biresolution match (map (pair false) (order_list krls)) i)
   27.74 -         else no_tac
   27.75 -      end);
   27.76 +  SUBGOAL (fn (prem,i) =>
   27.77 +    let val krls = Net.unify_term net (Logic.strip_assums_concl prem) in
   27.78 +      if pred krls then
   27.79 +        PRIMSEQ (Thm.biresolution NONE match (map (pair false) (order_list krls)) i)
   27.80 +      else no_tac
   27.81 +    end);
   27.82  
   27.83  (*Resolve the subgoal using the rules (making a net) unless too flexible,
   27.84     which means more than maxr rules are unifiable.      *)
    28.1 --- a/src/Pure/thm.ML	Sat Nov 08 17:39:01 2014 +0100
    28.2 +++ b/src/Pure/thm.ML	Sat Nov 08 21:31:51 2014 +0100
    28.3 @@ -115,7 +115,7 @@
    28.4    val combination: thm -> thm -> thm
    28.5    val equal_intr: thm -> thm -> thm
    28.6    val equal_elim: thm -> thm -> thm
    28.7 -  val flexflex_rule: thm -> thm Seq.seq
    28.8 +  val flexflex_rule: Proof.context option -> thm -> thm Seq.seq
    28.9    val generalize: string list * string list -> int -> thm -> thm
   28.10    val instantiate: (ctyp * ctyp) list * (cterm * cterm) list -> thm -> thm
   28.11    val instantiate_cterm: (ctyp * ctyp) list * (cterm * cterm) list -> cterm -> cterm
   28.12 @@ -128,15 +128,15 @@
   28.13    val legacy_freezeT: thm -> thm
   28.14    val lift_rule: cterm -> thm -> thm
   28.15    val incr_indexes: int -> thm -> thm
   28.16 -  val assumption: int -> thm -> thm Seq.seq
   28.17 +  val assumption: Proof.context option -> int -> thm -> thm Seq.seq
   28.18    val eq_assumption: int -> thm -> thm
   28.19    val rotate_rule: int -> int -> thm -> thm
   28.20    val permute_prems: int -> int -> thm -> thm
   28.21    val rename_params_rule: string list * int -> thm -> thm
   28.22    val rename_boundvars: term -> term -> thm -> thm
   28.23 -  val bicompose: {flatten: bool, match: bool, incremented: bool} ->
   28.24 +  val bicompose: Proof.context option -> {flatten: bool, match: bool, incremented: bool} ->
   28.25      bool * thm * int -> int -> thm -> thm Seq.seq
   28.26 -  val biresolution: bool -> (bool * thm) list -> int -> thm -> thm Seq.seq
   28.27 +  val biresolution: Proof.context option -> bool -> (bool * thm) list -> int -> thm -> thm Seq.seq
   28.28    val extern_oracles: Proof.context -> (Markup.T * xstring) list
   28.29    val add_oracle: binding * ('a -> cterm) -> theory -> (string * ('a -> thm)) * theory
   28.30  end;
   28.31 @@ -415,6 +415,11 @@
   28.32          prop = prop})
   28.33    end;
   28.34  
   28.35 +fun make_context NONE thy = Context.Theory thy
   28.36 +  | make_context (SOME ctxt) thy =
   28.37 +      if Theory.subthy (thy, Proof_Context.theory_of ctxt) then Context.Proof ctxt
   28.38 +      else raise THEORY ("Bad context", [thy, Proof_Context.theory_of ctxt]);
   28.39 +
   28.40  (*explicit weakening: maps |- B to A |- B*)
   28.41  fun weaken raw_ct th =
   28.42    let
   28.43 @@ -989,8 +994,8 @@
   28.44    Instantiates the theorem and deletes trivial tpairs.  Resulting
   28.45    sequence may contain multiple elements if the tpairs are not all
   28.46    flex-flex.*)
   28.47 -fun flexflex_rule (th as Thm (der, {thy, maxidx, shyps, hyps, tpairs, prop, ...})) =
   28.48 -  Unify.smash_unifiers thy tpairs (Envir.empty maxidx)
   28.49 +fun flexflex_rule opt_ctxt (th as Thm (der, {thy, maxidx, shyps, hyps, tpairs, prop, ...})) =
   28.50 +  Unify.smash_unifiers (make_context opt_ctxt thy) tpairs (Envir.empty maxidx)
   28.51    |> Seq.map (fn env =>
   28.52        if Envir.is_empty env then th
   28.53        else
   28.54 @@ -1304,9 +1309,10 @@
   28.55        prop = Logic.incr_indexes ([], i) prop});
   28.56  
   28.57  (*Solve subgoal Bi of proof state B1...Bn/C by assumption. *)
   28.58 -fun assumption i state =
   28.59 +fun assumption opt_ctxt i state =
   28.60    let
   28.61      val Thm (der, {thy, maxidx, shyps, hyps, ...}) = state;
   28.62 +    val context = make_context opt_ctxt thy;
   28.63      val (tpairs, Bs, Bi, C) = dest_state (state, i);
   28.64      fun newth n (env, tpairs) =
   28.65        Thm (deriv_rule1
   28.66 @@ -1332,7 +1338,7 @@
   28.67        | addprfs (asm :: rest) n = Seq.make (fn () => Seq.pull
   28.68            (Seq.mapp (newth n)
   28.69              (if Term.could_unify (asm, concl) then
   28.70 -              (Unify.unifiers (thy, Envir.empty maxidx, (close asm, concl') :: tpairs))
   28.71 +              (Unify.unifiers (context, Envir.empty maxidx, (close asm, concl') :: tpairs))
   28.72               else Seq.empty)
   28.73              (addprfs rest (n + 1))))
   28.74    in addprfs asms 1 end;
   28.75 @@ -1555,9 +1561,9 @@
   28.76  
   28.77  
   28.78  (*unify types of schematic variables (non-lifted case)*)
   28.79 -fun unify_var_types thy (th1, th2) env =
   28.80 +fun unify_var_types context (th1, th2) env =
   28.81    let
   28.82 -    fun unify_vars (T :: Us) = fold (fn U => Pattern.unify_types thy (T, U)) Us
   28.83 +    fun unify_vars (T :: Us) = fold (fn U => Pattern.unify_types context (T, U)) Us
   28.84        | unify_vars _ = I;
   28.85      val add_vars =
   28.86        full_prop_of #>
   28.87 @@ -1576,7 +1582,7 @@
   28.88  *)
   28.89  local exception COMPOSE
   28.90  in
   28.91 -fun bicompose_aux {flatten, match, incremented} (state, (stpairs, Bs, Bi, C), lifted)
   28.92 +fun bicompose_aux opt_ctxt {flatten, match, incremented} (state, (stpairs, Bs, Bi, C), lifted)
   28.93                          (eres_flg, orule, nsubgoal) =
   28.94   let val Thm (sder, {maxidx=smax, shyps=sshyps, hyps=shyps, ...}) = state
   28.95       and Thm (rder, {maxidx=rmax, shyps=rshyps, hyps=rhyps,
   28.96 @@ -1584,6 +1590,7 @@
   28.97           (*How many hyps to skip over during normalization*)
   28.98       and nlift = Logic.count_prems (strip_all_body Bi) + (if eres_flg then ~1 else 0)
   28.99       val thy = merge_thys2 state orule;
  28.100 +     val context = make_context opt_ctxt thy;
  28.101       (** Add new theorem with prop = '[| Bs; As |] ==> C' to thq **)
  28.102       fun addth A (As, oldAs, rder', n) ((env, tpairs), thq) =
  28.103         let val normt = Envir.norm_term env;
  28.104 @@ -1646,7 +1653,7 @@
  28.105                 | tryasms (asm :: rest) n =
  28.106                     if Term.could_unify (asm, concl) then
  28.107                       let val asm' = close asm in
  28.108 -                       (case Seq.pull (Unify.unifiers (thy, env, (asm', concl') :: dpairs)) of
  28.109 +                       (case Seq.pull (Unify.unifiers (context, env, (asm', concl') :: dpairs)) of
  28.110                           NONE => tryasms rest (n + 1)
  28.111                         | cell as SOME ((_, tpairs), _) =>
  28.112                             Seq.it_right (addth A (newAs (As, n, [BBi, (concl', asm')], tpairs)))
  28.113 @@ -1658,7 +1665,7 @@
  28.114  
  28.115       (*ordinary resolution*)
  28.116       fun res env =
  28.117 -       (case Seq.pull (Unify.unifiers (thy, env, dpairs)) of
  28.118 +       (case Seq.pull (Unify.unifiers (context, env, dpairs)) of
  28.119           NONE => Seq.empty
  28.120         | cell as SOME ((_, tpairs), _) =>
  28.121             Seq.it_right (addth NONE (newAs (rev rAs, 0, [BBi], tpairs)))
  28.122 @@ -1666,14 +1673,14 @@
  28.123  
  28.124       val env0 = Envir.empty (Int.max (rmax, smax));
  28.125   in
  28.126 -   (case if incremented then SOME env0 else unify_var_types thy (state, orule) env0 of
  28.127 +   (case if incremented then SOME env0 else unify_var_types context (state, orule) env0 of
  28.128       NONE => Seq.empty
  28.129     | SOME env => if eres_flg then eres env (rev rAs) else res env)
  28.130   end;
  28.131  end;
  28.132  
  28.133 -fun bicompose flags arg i state =
  28.134 -  bicompose_aux flags (state, dest_state (state,i), false) arg;
  28.135 +fun bicompose opt_ctxt flags arg i state =
  28.136 +  bicompose_aux opt_ctxt flags (state, dest_state (state,i), false) arg;
  28.137  
  28.138  (*Quick test whether rule is resolvable with the subgoal with hyps Hs
  28.139    and conclusion B.  If eres_flg then checks 1st premise of rule also*)
  28.140 @@ -1686,18 +1693,18 @@
  28.141  
  28.142  (*Bi-resolution of a state with a list of (flag,rule) pairs.
  28.143    Puts the rule above:  rule/state.  Renames vars in the rules. *)
  28.144 -fun biresolution match brules i state =
  28.145 +fun biresolution opt_ctxt match brules i state =
  28.146      let val (stpairs, Bs, Bi, C) = dest_state(state,i);
  28.147          val lift = lift_rule (cprem_of state i);
  28.148          val B = Logic.strip_assums_concl Bi;
  28.149          val Hs = Logic.strip_assums_hyp Bi;
  28.150          val compose =
  28.151 -          bicompose_aux {flatten = true, match = match, incremented = true}
  28.152 +          bicompose_aux opt_ctxt {flatten = true, match = match, incremented = true}
  28.153              (state, (stpairs, Bs, Bi, C), true);
  28.154          fun res [] = Seq.empty
  28.155            | res ((eres_flg, rule)::brules) =
  28.156 -              if Config.get_global (theory_of_thm state) Pattern.unify_trace_failure orelse
  28.157 -                 could_bires (Hs, B, eres_flg, rule)
  28.158 +              if Config.get_generic (make_context opt_ctxt (theory_of_thm state))
  28.159 +                  Pattern.unify_trace_failure orelse could_bires (Hs, B, eres_flg, rule)
  28.160                then Seq.make (*delay processing remainder till needed*)
  28.161                    (fn()=> SOME(compose (eres_flg, lift rule, nprems_of rule),
  28.162                                 res brules))
    29.1 --- a/src/Pure/unify.ML	Sat Nov 08 17:39:01 2014 +0100
    29.2 +++ b/src/Pure/unify.ML	Sat Nov 08 21:31:51 2014 +0100
    29.3 @@ -19,13 +19,13 @@
    29.4    val trace_simp: bool Config.T
    29.5    val trace_types_raw: Config.raw
    29.6    val trace_types: bool Config.T
    29.7 -  val hounifiers: theory * Envir.env * ((term * term) list) ->
    29.8 +  val hounifiers: Context.generic * Envir.env * ((term * term) list) ->
    29.9      (Envir.env * (term * term) list) Seq.seq
   29.10 -  val unifiers: theory * Envir.env * ((term * term) list) ->
   29.11 +  val unifiers: Context.generic * Envir.env * ((term * term) list) ->
   29.12      (Envir.env * (term * term) list) Seq.seq
   29.13 -  val smash_unifiers: theory -> (term * term) list -> Envir.env -> Envir.env Seq.seq
   29.14 -  val matchers: theory -> (term * term) list -> Envir.env Seq.seq
   29.15 -  val matches_list: theory -> term list -> term list -> bool
   29.16 +  val smash_unifiers: Context.generic -> (term * term) list -> Envir.env -> Envir.env Seq.seq
   29.17 +  val matchers: Context.generic -> (term * term) list -> Envir.env Seq.seq
   29.18 +  val matches_list: Context.generic -> term list -> term list -> bool
   29.19  end
   29.20  
   29.21  structure Unify : UNIFY =
   29.22 @@ -34,19 +34,19 @@
   29.23  (*Unification options*)
   29.24  
   29.25  (*tracing starts above this depth, 0 for full*)
   29.26 -val trace_bound_raw = Config.declare_global ("unify_trace_bound", @{here}) (K (Config.Int 50));
   29.27 +val trace_bound_raw = Config.declare ("unify_trace_bound", @{here}) (K (Config.Int 50));
   29.28  val trace_bound = Config.int trace_bound_raw;
   29.29  
   29.30  (*unification quits above this depth*)
   29.31 -val search_bound_raw = Config.declare_global ("unify_search_bound", @{here}) (K (Config.Int 60));
   29.32 +val search_bound_raw = Config.declare ("unify_search_bound", @{here}) (K (Config.Int 60));
   29.33  val search_bound = Config.int search_bound_raw;
   29.34  
   29.35  (*print dpairs before calling SIMPL*)
   29.36 -val trace_simp_raw = Config.declare_global ("unify_trace_simp", @{here}) (K (Config.Bool false));
   29.37 +val trace_simp_raw = Config.declare ("unify_trace_simp", @{here}) (K (Config.Bool false));
   29.38  val trace_simp = Config.bool trace_simp_raw;
   29.39  
   29.40  (*announce potential incompleteness of type unification*)
   29.41 -val trace_types_raw = Config.declare_global ("unify_trace_types", @{here}) (K (Config.Bool false));
   29.42 +val trace_types_raw = Config.declare ("unify_trace_types", @{here}) (K (Config.Bool false));
   29.43  val trace_types = Config.bool trace_types_raw;
   29.44  
   29.45  
   29.46 @@ -183,18 +183,18 @@
   29.47  exception ASSIGN;  (*Raised if not an assignment*)
   29.48  
   29.49  
   29.50 -fun unify_types thy TU env =
   29.51 -  Pattern.unify_types thy TU env handle Pattern.Unif => raise CANTUNIFY;
   29.52 +fun unify_types context TU env =
   29.53 +  Pattern.unify_types context TU env handle Pattern.Unif => raise CANTUNIFY;
   29.54  
   29.55 -fun test_unify_types thy (T, U) env =
   29.56 +fun test_unify_types context (T, U) env =
   29.57    let
   29.58 -    val str_of = Syntax.string_of_typ_global thy;
   29.59 -    fun warn () =
   29.60 -      if Context_Position.is_visible_global thy then
   29.61 -        tracing ("Potential loss of completeness: " ^ str_of U ^ " = " ^ str_of T)
   29.62 +    fun trace () =
   29.63 +      if Context_Position.is_visible_generic context then
   29.64 +        let val str_of = Syntax.string_of_typ (Context.proof_of context)
   29.65 +        in tracing ("Potential loss of completeness: " ^ str_of U ^ " = " ^ str_of T) end
   29.66        else ();
   29.67 -    val env' = unify_types thy (T, U) env;
   29.68 -  in if is_TVar T orelse is_TVar U then warn () else (); env' end;
   29.69 +    val env' = unify_types context (T, U) env;
   29.70 +  in if is_TVar T orelse is_TVar U then trace () else (); env' end;
   29.71  
   29.72  (*Is the term eta-convertible to a single variable with the given rbinder?
   29.73    Examples: ?a   ?f(B.0)   ?g(B.1,B.0)
   29.74 @@ -209,11 +209,11 @@
   29.75  (*Solve v=u by assignment -- "fixedpoint" to Huet -- if v not in u.
   29.76    If v occurs rigidly then nonunifiable.
   29.77    If v occurs nonrigidly then must use full algorithm. *)
   29.78 -fun assignment thy (rbinder, t, u) env =
   29.79 +fun assignment context (rbinder, t, u) env =
   29.80    let val vT as (v,T) = get_eta_var (rbinder, 0, t) in
   29.81      (case rigid_occurs_term (Unsynchronized.ref [], env, v, u) of
   29.82        NoOcc =>
   29.83 -        let val env = unify_types thy (Envir.body_type env T, fastype env (rbinder, u)) env
   29.84 +        let val env = unify_types context (Envir.body_type env T, fastype env (rbinder, u)) env
   29.85          in Envir.update (vT, Logic.rlist_abs (rbinder, u)) env end
   29.86      | Nonrigid => raise ASSIGN
   29.87      | Rigid => raise CANTUNIFY)
   29.88 @@ -225,18 +225,18 @@
   29.89    Checks that binders have same length, since terms should be eta-normal;
   29.90      if not, raises TERM, probably indicating type mismatch.
   29.91    Uses variable a (unless the null string) to preserve user's naming.*)
   29.92 -fun new_dpair thy (rbinder, Abs (a, T, body1), Abs (b, U, body2)) env =
   29.93 +fun new_dpair context (rbinder, Abs (a, T, body1), Abs (b, U, body2)) env =
   29.94        let
   29.95 -        val env' = unify_types thy (T, U) env;
   29.96 +        val env' = unify_types context (T, U) env;
   29.97          val c = if a = "" then b else a;
   29.98 -      in new_dpair thy ((c,T) :: rbinder, body1, body2) env' end
   29.99 +      in new_dpair context ((c,T) :: rbinder, body1, body2) env' end
  29.100    | new_dpair _ (_, Abs _, _) _ = raise TERM ("new_dpair", [])
  29.101    | new_dpair _ (_, _, Abs _) _ = raise TERM ("new_dpair", [])
  29.102    | new_dpair _ (rbinder, t1, t2) env = ((rbinder, t1, t2), env);
  29.103  
  29.104  
  29.105 -fun head_norm_dpair thy (env, (rbinder, t, u)) : dpair * Envir.env =
  29.106 -  new_dpair thy (rbinder,
  29.107 +fun head_norm_dpair context (env, (rbinder, t, u)) : dpair * Envir.env =
  29.108 +  new_dpair context (rbinder,
  29.109      eta_norm env (rbinder, Envir.head_norm env t),
  29.110      eta_norm env (rbinder, Envir.head_norm env u)) env;
  29.111  
  29.112 @@ -248,11 +248,11 @@
  29.113    Does not even identify Vars in dpairs such as ?a =?= ?b; an attempt to
  29.114      do so caused numerous problems with no compensating advantage.
  29.115  *)
  29.116 -fun SIMPL0 thy dp0 (env,flexflex,flexrigid) : Envir.env * dpair list * dpair list =
  29.117 +fun SIMPL0 context dp0 (env,flexflex,flexrigid) : Envir.env * dpair list * dpair list =
  29.118    let
  29.119 -    val (dp as (rbinder, t, u), env) = head_norm_dpair thy (env, dp0);
  29.120 +    val (dp as (rbinder, t, u), env) = head_norm_dpair context (env, dp0);
  29.121      fun SIMRANDS (f $ t, g $ u, env) =
  29.122 -          SIMPL0 thy (rbinder, t, u) (SIMRANDS (f, g, env))
  29.123 +          SIMPL0 context (rbinder, t, u) (SIMRANDS (f, g, env))
  29.124        | SIMRANDS (t as _$_, _, _) =
  29.125            raise TERM ("SIMPL: operands mismatch", [t, u])
  29.126        | SIMRANDS (t, u as _ $ _, _) =
  29.127 @@ -263,21 +263,21 @@
  29.128        (Var (_, T), Var (_, U)) =>
  29.129          let
  29.130            val T' = Envir.body_type env T and U' = Envir.body_type env U;
  29.131 -          val env = unify_types thy (T', U') env;
  29.132 +          val env = unify_types context (T', U') env;
  29.133          in (env, dp :: flexflex, flexrigid) end
  29.134      | (Var _, _) =>
  29.135 -        ((assignment thy (rbinder,t,u) env, flexflex, flexrigid)
  29.136 +        ((assignment context (rbinder,t,u) env, flexflex, flexrigid)
  29.137            handle ASSIGN => (env, flexflex, dp :: flexrigid))
  29.138      | (_, Var _) =>
  29.139 -        ((assignment thy (rbinder, u, t) env, flexflex, flexrigid)
  29.140 +        ((assignment context (rbinder, u, t) env, flexflex, flexrigid)
  29.141            handle ASSIGN => (env, flexflex, (rbinder, u, t) :: flexrigid))
  29.142      | (Const (a, T), Const (b, U)) =>
  29.143 -        if a = b then SIMRANDS (t, u, unify_types thy (T, U) env)
  29.144 +        if a = b then SIMRANDS (t, u, unify_types context (T, U) env)
  29.145          else raise CANTUNIFY
  29.146      | (Bound i, Bound j) =>
  29.147          if i = j then SIMRANDS (t, u, env) else raise CANTUNIFY
  29.148      | (Free (a, T), Free (b, U)) =>
  29.149 -        if a = b then SIMRANDS (t, u, unify_types thy (T, U) env)
  29.150 +        if a = b then SIMRANDS (t, u, unify_types context (T, U) env)
  29.151          else raise CANTUNIFY
  29.152      | _ => raise CANTUNIFY)
  29.153    end;
  29.154 @@ -291,13 +291,13 @@
  29.155  
  29.156  (*Recursion needed if any of the 'head variables' have been updated
  29.157    Clever would be to re-do just the affected dpairs*)
  29.158 -fun SIMPL thy (env,dpairs) : Envir.env * dpair list * dpair list =
  29.159 +fun SIMPL context (env,dpairs) : Envir.env * dpair list * dpair list =
  29.160    let
  29.161 -    val all as (env', flexflex, flexrigid) = fold_rev (SIMPL0 thy) dpairs (env, [], []);
  29.162 +    val all as (env', flexflex, flexrigid) = fold_rev (SIMPL0 context) dpairs (env, [], []);
  29.163      val dps = flexrigid @ flexflex;
  29.164    in
  29.165      if exists (fn (_, t, u) => changed env' t orelse changed env' u) dps
  29.166 -    then SIMPL thy (env', dps) else all
  29.167 +    then SIMPL context (env', dps) else all
  29.168    end;
  29.169  
  29.170  
  29.171 @@ -331,11 +331,11 @@
  29.172    For example, projection in ?b'(?a) may be wrong if other dpairs constrain ?a.
  29.173    The order for trying projections is crucial in ?b'(?a)
  29.174    NB "vname" is only used in the call to make_args!!   *)
  29.175 -fun matchcopy thy vname =
  29.176 +fun matchcopy context vname =
  29.177    let
  29.178      fun mc (rbinder, targs, u, ed as (env, dpairs)) : (term * (Envir.env * dpair list)) Seq.seq =
  29.179        let
  29.180 -        val trace_types = Config.get_global thy trace_types;
  29.181 +        val trace_types = Config.get_generic context trace_types;
  29.182          (*Produce copies of uarg and cons them in front of uargs*)
  29.183          fun copycons uarg (uargs, (env, dpairs)) =
  29.184            Seq.map (fn (uarg', ed') => (uarg' :: uargs, ed'))
  29.185 @@ -352,8 +352,8 @@
  29.186          fun projenv (head, (Us, bary), targ, tail) =
  29.187            let
  29.188              val env =
  29.189 -              if trace_types then test_unify_types thy (base, bary) env
  29.190 -              else unify_types thy (base, bary) env
  29.191 +              if trace_types then test_unify_types context (base, bary) env
  29.192 +              else unify_types context (base, bary) env
  29.193            in
  29.194              Seq.make (fn () =>
  29.195                let
  29.196 @@ -361,7 +361,7 @@
  29.197                  (*higher-order projection: plug in targs for bound vars*)
  29.198                  fun plugin arg = list_comb (head_of arg, targs);
  29.199                  val dp = (rbinder, list_comb (targ, map plugin args), u);
  29.200 -                val (env2, frigid, fflex) = SIMPL thy (env', dp :: dpairs);
  29.201 +                val (env2, frigid, fflex) = SIMPL context (env', dp :: dpairs);
  29.202                  (*may raise exception CANTUNIFY*)
  29.203                in
  29.204                  SOME ((list_comb (head, args), (env2, frigid @ fflex)), tail)
  29.205 @@ -398,7 +398,7 @@
  29.206  
  29.207  
  29.208  (*Call matchcopy to produce assignments to the variable in the dpair*)
  29.209 -fun MATCH thy (env, (rbinder, t, u), dpairs) : (Envir.env * dpair list) Seq.seq =
  29.210 +fun MATCH context (env, (rbinder, t, u), dpairs) : (Envir.env * dpair list) Seq.seq =
  29.211    let
  29.212      val (Var (vT as (v, T)), targs) = strip_comb t;
  29.213      val Ts = Envir.binder_types env T;
  29.214 @@ -408,7 +408,7 @@
  29.215          NONE => (Envir.update (vT, types_abs (Ts, u')) env', dpairs')
  29.216        | SOME s => (env', ([], s, types_abs (Ts, u')) :: dpairs'));
  29.217    in
  29.218 -    Seq.map new_dset (matchcopy thy (#1 v) (rbinder, targs, u, (env, dpairs)))
  29.219 +    Seq.map new_dset (matchcopy context (#1 v) (rbinder, targs, u, (env, dpairs)))
  29.220    end;
  29.221  
  29.222  
  29.223 @@ -417,11 +417,11 @@
  29.224  
  29.225  (*At end of unification, do flex-flex assignments like ?a -> ?f(?b)
  29.226    Attempts to update t with u, raising ASSIGN if impossible*)
  29.227 -fun ff_assign thy (env, rbinder, t, u) : Envir.env =
  29.228 +fun ff_assign context (env, rbinder, t, u) : Envir.env =
  29.229    let val vT as (v, T) = get_eta_var (rbinder, 0, t) in
  29.230      if occurs_terms (Unsynchronized.ref [], env, v, [u]) then raise ASSIGN
  29.231      else
  29.232 -      let val env = unify_types thy (Envir.body_type env T, fastype env (rbinder, u)) env
  29.233 +      let val env = unify_types context (Envir.body_type env T, fastype env (rbinder, u)) env
  29.234        in Envir.vupdate (vT, Logic.rlist_abs (rbinder, u)) env end
  29.235    end;
  29.236  
  29.237 @@ -531,7 +531,7 @@
  29.238  
  29.239  (*Simplify both terms and check for assignments.
  29.240    Bound vars in the binder are "banned" unless used in both t AND u *)
  29.241 -fun clean_ffpair thy ((rbinder, t, u), (env, tpairs)) =
  29.242 +fun clean_ffpair context ((rbinder, t, u), (env, tpairs)) =
  29.243    let
  29.244      val loot = loose_bnos t and loou = loose_bnos u
  29.245      fun add_index (j, (a, T)) (bnos, newbinder) =
  29.246 @@ -542,9 +542,9 @@
  29.247      val (env', t') = clean_term banned (env, t);
  29.248      val (env'',u') = clean_term banned (env',u);
  29.249    in
  29.250 -    (ff_assign thy (env'', rbin', t', u'), tpairs)
  29.251 +    (ff_assign context (env'', rbin', t', u'), tpairs)
  29.252        handle ASSIGN =>
  29.253 -        (ff_assign thy (env'', rbin', u', t'), tpairs)
  29.254 +        (ff_assign context (env'', rbin', u', t'), tpairs)
  29.255            handle ASSIGN => (env'', add_tpair (rbin', (t', u'), tpairs))
  29.256    end
  29.257    handle CHANGE_FAIL => (env, add_tpair (rbinder, (t, u), tpairs));
  29.258 @@ -554,7 +554,7 @@
  29.259    eliminates trivial tpairs like t=t, as well as repeated ones
  29.260    trivial tpairs can easily escape SIMPL:  ?A=t, ?A=?B, ?B=t gives t=t
  29.261    Resulting tpairs MAY NOT be in normal form:  assignments may occur here.*)
  29.262 -fun add_ffpair thy (rbinder,t0,u0) (env,tpairs) : Envir.env * (term * term) list =
  29.263 +fun add_ffpair context (rbinder,t0,u0) (env,tpairs) : Envir.env * (term * term) list =
  29.264    let
  29.265      val t = Envir.norm_term env t0
  29.266      and u = Envir.norm_term env u0;
  29.267 @@ -565,8 +565,8 @@
  29.268            if T = U then (env, add_tpair (rbinder, (t, u), tpairs))
  29.269            else raise TERM ("add_ffpair: Var name confusion", [t, u])
  29.270          else if Term_Ord.indexname_ord (v, w) = LESS then (*prefer to update the LARGER variable*)
  29.271 -          clean_ffpair thy ((rbinder, u, t), (env, tpairs))
  29.272 -        else clean_ffpair thy ((rbinder, t, u), (env, tpairs))
  29.273 +          clean_ffpair context ((rbinder, u, t), (env, tpairs))
  29.274 +        else clean_ffpair context ((rbinder, t, u), (env, tpairs))
  29.275      | _ => raise TERM ("add_ffpair: Vars expected", [t, u]))
  29.276    end;
  29.277  
  29.278 @@ -574,15 +574,16 @@
  29.279  (*Print a tracing message + list of dpairs.
  29.280    In t==u print u first because it may be rigid or flexible --
  29.281      t is always flexible.*)
  29.282 -fun print_dpairs thy msg (env, dpairs) =
  29.283 -  if Context_Position.is_visible_global thy then
  29.284 +fun print_dpairs context msg (env, dpairs) =
  29.285 +  if Context_Position.is_visible_generic context then
  29.286      let
  29.287        fun pdp (rbinder, t, u) =
  29.288          let
  29.289 +          val ctxt = Context.proof_of context;
  29.290            fun termT t =
  29.291 -            Syntax.pretty_term_global thy (Envir.norm_term env (Logic.rlist_abs (rbinder, t)));
  29.292 -          val bsymbs = [termT u, Pretty.str " =?=", Pretty.brk 1, termT t];
  29.293 -        in tracing (Pretty.string_of (Pretty.blk (0, bsymbs))) end;
  29.294 +            Syntax.pretty_term ctxt (Envir.norm_term env (Logic.rlist_abs (rbinder, t)));
  29.295 +          val prt = Pretty.blk (0, [termT u, Pretty.str " =?=", Pretty.brk 1, termT t]);
  29.296 +        in tracing (Pretty.string_of prt) end;
  29.297      in tracing msg; List.app pdp dpairs end
  29.298    else ();
  29.299  
  29.300 @@ -590,41 +591,41 @@
  29.301  (*Unify the dpairs in the environment.
  29.302    Returns flex-flex disagreement pairs NOT IN normal form.
  29.303    SIMPL may raise exception CANTUNIFY. *)
  29.304 -fun hounifiers (thy, env, tus : (term * term) list) : (Envir.env * (term * term) list) Seq.seq =
  29.305 +fun hounifiers (context, env, tus : (term * term) list) : (Envir.env * (term * term) list) Seq.seq =
  29.306    let
  29.307 -    val trace_bound = Config.get_global thy trace_bound;
  29.308 -    val search_bound = Config.get_global thy search_bound;
  29.309 -    val trace_simp = Config.get_global thy trace_simp;
  29.310 +    val trace_bound = Config.get_generic context trace_bound;
  29.311 +    val search_bound = Config.get_generic context search_bound;
  29.312 +    val trace_simp = Config.get_generic context trace_simp;
  29.313      fun add_unify tdepth ((env, dpairs), reseq) =
  29.314        Seq.make (fn () =>
  29.315          let
  29.316            val (env', flexflex, flexrigid) =
  29.317             (if tdepth > trace_bound andalso trace_simp
  29.318 -            then print_dpairs thy "Enter SIMPL" (env, dpairs) else ();
  29.319 -            SIMPL thy (env, dpairs));
  29.320 +            then print_dpairs context "Enter SIMPL" (env, dpairs) else ();
  29.321 +            SIMPL context (env, dpairs));
  29.322          in
  29.323            (case flexrigid of
  29.324 -            [] => SOME (fold_rev (add_ffpair thy) flexflex (env', []), reseq)
  29.325 +            [] => SOME (fold_rev (add_ffpair context) flexflex (env', []), reseq)
  29.326            | dp :: frigid' =>
  29.327                if tdepth > search_bound then
  29.328 -                (if Context_Position.is_visible_global thy
  29.329 +                (if Context_Position.is_visible_generic context
  29.330                   then warning "Unification bound exceeded" else (); Seq.pull reseq)
  29.331                else
  29.332                 (if tdepth > trace_bound then
  29.333 -                  print_dpairs thy "Enter MATCH" (env',flexrigid@flexflex)
  29.334 +                  print_dpairs context "Enter MATCH" (env',flexrigid@flexflex)
  29.335                  else ();
  29.336                  Seq.pull (Seq.it_right
  29.337 -                    (add_unify (tdepth + 1)) (MATCH thy (env',dp, frigid'@flexflex), reseq))))
  29.338 +                    (add_unify (tdepth + 1)) (MATCH context (env',dp, frigid'@flexflex), reseq))))
  29.339          end
  29.340          handle CANTUNIFY =>
  29.341 -         (if tdepth > trace_bound andalso Context_Position.is_visible_global thy
  29.342 +         (if tdepth > trace_bound andalso Context_Position.is_visible_generic context
  29.343            then tracing "Failure node"
  29.344            else (); Seq.pull reseq));
  29.345      val dps = map (fn (t, u) => ([], t, u)) tus;
  29.346    in add_unify 1 ((env, dps), Seq.empty) end;
  29.347  
  29.348 -fun unifiers (params as (thy, env, tus)) =
  29.349 -  Seq.cons (fold (Pattern.unify thy) tus env, []) Seq.empty
  29.350 +fun unifiers (params as (context, env, tus)) =
  29.351 +  Seq.cons (fold (Pattern.unify context) tus env, []) Seq.empty
  29.352      handle Pattern.Unif => Seq.empty
  29.353        | Pattern.Pattern => hounifiers params;
  29.354  
  29.355 @@ -660,8 +661,8 @@
  29.356    fold_rev smash_flexflex1 tpairs env;
  29.357  
  29.358  (*Returns unifiers with no remaining disagreement pairs*)
  29.359 -fun smash_unifiers thy tus env =
  29.360 -  Seq.map smash_flexflex (unifiers (thy, env, tus));
  29.361 +fun smash_unifiers context tus env =
  29.362 +  Seq.map smash_flexflex (unifiers (context, env, tus));
  29.363  
  29.364  
  29.365  (*Pattern matching*)
  29.366 @@ -672,8 +673,10 @@
  29.367  
  29.368  (*General matching -- keep variables disjoint*)
  29.369  fun matchers _ [] = Seq.single (Envir.empty ~1)
  29.370 -  | matchers thy pairs =
  29.371 +  | matchers context pairs =
  29.372        let
  29.373 +        val thy = Context.theory_of context;
  29.374 +
  29.375          val maxidx = fold (Term.maxidx_term o #2) pairs ~1;
  29.376          val offset = maxidx + 1;
  29.377          val pairs' = map (apfst (Logic.incr_indexes ([], offset))) pairs;
  29.378 @@ -719,11 +722,11 @@
  29.379          val empty = Envir.empty maxidx';
  29.380        in
  29.381          Seq.append
  29.382 -          (Seq.map_filter result (smash_unifiers thy pairs' empty))
  29.383 +          (Seq.map_filter result (smash_unifiers context pairs' empty))
  29.384            (first_order_matchers thy pairs empty)
  29.385        end;
  29.386  
  29.387 -fun matches_list thy ps os =
  29.388 -  length ps = length os andalso is_some (Seq.pull (matchers thy (ps ~~ os)));
  29.389 +fun matches_list context ps os =
  29.390 +  length ps = length os andalso is_some (Seq.pull (matchers context (ps ~~ os)));
  29.391  
  29.392  end;
    30.1 --- a/src/Tools/eqsubst.ML	Sat Nov 08 17:39:01 2014 +0100
    30.2 +++ b/src/Tools/eqsubst.ML	Sat Nov 08 21:31:51 2014 +0100
    30.3 @@ -161,7 +161,7 @@
    30.4               Vartab.dest (Envir.term_env env));
    30.5            val initenv =
    30.6              Envir.Envir {maxidx = ix2, tenv = Vartab.empty, tyenv = typinsttab};
    30.7 -          val useq = Unify.smash_unifiers thy [a] initenv
    30.8 +          val useq = Unify.smash_unifiers (Context.Theory thy) [a] initenv
    30.9              handle ListPair.UnequalLengths => Seq.empty
   30.10                | Term.TERM _ => Seq.empty;
   30.11            fun clean_unify' useq () =
    31.1 --- a/src/Tools/induct.ML	Sat Nov 08 17:39:01 2014 +0100
    31.2 +++ b/src/Tools/induct.ML	Sat Nov 08 21:31:51 2014 +0100
    31.3 @@ -602,7 +602,8 @@
    31.4          val rule' = Thm.incr_indexes (maxidx + 1) rule;
    31.5          val concl = Logic.strip_assums_concl goal;
    31.6        in
    31.7 -        Unify.smash_unifiers thy [(Thm.concl_of rule', concl)] (Envir.empty (Thm.maxidx_of rule'))
    31.8 +        Unify.smash_unifiers (Context.Proof ctxt)
    31.9 +          [(Thm.concl_of rule', concl)] (Envir.empty (Thm.maxidx_of rule'))
   31.10          |> Seq.map (fn env => Drule.instantiate_normalize (dest_env thy env) rule')
   31.11        end
   31.12    end
    32.1 --- a/src/Tools/misc_legacy.ML	Sat Nov 08 17:39:01 2014 +0100
    32.2 +++ b/src/Tools/misc_legacy.ML	Sat Nov 08 21:31:51 2014 +0100
    32.3 @@ -204,7 +204,7 @@
    32.4          end
    32.5        (*function to replace the current subgoal*)
    32.6        fun next st =
    32.7 -        Thm.bicompose {flatten = true, match = false, incremented = false}
    32.8 +        Thm.bicompose NONE {flatten = true, match = false, incremented = false}
    32.9            (false, relift st, nprems_of st) gno state
   32.10    in Seq.maps next (tacf subprems (Thm.trivial (cterm concl))) end;
   32.11