# HG changeset patch
# User wenzelm
# Date 1132159530 -3600
# Node ID 43c4589a9a7856d4b502613c639f0b8684868aef
# Parent  a9f67248996a737ce92d49c002972c2929b95d5c
tuned Pattern.match/unify;

diff -r a9f67248996a -r 43c4589a9a78 TFL/rules.ML
--- a/TFL/rules.ML	Wed Nov 16 17:45:29 2005 +0100
+++ b/TFL/rules.ML	Wed Nov 16 17:45:30 2005 +0100
@@ -8,56 +8,56 @@
 
 signature RULES =
 sig
-  val dest_thm : thm -> term list * term
+  val dest_thm: thm -> term list * term
 
   (* Inference rules *)
-  val REFL      :cterm -> thm
-  val ASSUME    :cterm -> thm
-  val MP        :thm -> thm -> thm
-  val MATCH_MP  :thm -> thm -> thm
-  val CONJUNCT1 :thm -> thm
-  val CONJUNCT2 :thm -> thm
-  val CONJUNCTS :thm -> thm list
-  val DISCH     :cterm -> thm -> thm
-  val UNDISCH   :thm  -> thm
-  val SPEC      :cterm -> thm -> thm
-  val ISPEC     :cterm -> thm -> thm
-  val ISPECL    :cterm list -> thm -> thm
-  val GEN       :cterm -> thm -> thm
-  val GENL      :cterm list -> thm -> thm
-  val LIST_CONJ :thm list -> thm
+  val REFL: cterm -> thm
+  val ASSUME: cterm -> thm
+  val MP: thm -> thm -> thm
+  val MATCH_MP: thm -> thm -> thm
+  val CONJUNCT1: thm -> thm
+  val CONJUNCT2: thm -> thm
+  val CONJUNCTS: thm -> thm list
+  val DISCH: cterm -> thm -> thm
+  val UNDISCH: thm  -> thm
+  val SPEC: cterm -> thm -> thm
+  val ISPEC: cterm -> thm -> thm
+  val ISPECL: cterm list -> thm -> thm
+  val GEN: cterm -> thm -> thm
+  val GENL: cterm list -> thm -> thm
+  val LIST_CONJ: thm list -> thm
 
-  val SYM : thm -> thm
-  val DISCH_ALL : thm -> thm
-  val FILTER_DISCH_ALL : (term -> bool) -> thm -> thm
-  val SPEC_ALL  : thm -> thm
-  val GEN_ALL   : thm -> thm
-  val IMP_TRANS : thm -> thm -> thm
-  val PROVE_HYP : thm -> thm -> thm
+  val SYM: thm -> thm
+  val DISCH_ALL: thm -> thm
+  val FILTER_DISCH_ALL: (term -> bool) -> thm -> thm
+  val SPEC_ALL: thm -> thm
+  val GEN_ALL: thm -> thm
+  val IMP_TRANS: thm -> thm -> thm
+  val PROVE_HYP: thm -> thm -> thm
 
-  val CHOOSE : cterm * thm -> thm -> thm
-  val EXISTS : cterm * cterm -> thm -> thm
-  val EXISTL : cterm list -> thm -> thm
-  val IT_EXISTS : (cterm*cterm) list -> thm -> thm
+  val CHOOSE: cterm * thm -> thm -> thm
+  val EXISTS: cterm * cterm -> thm -> thm
+  val EXISTL: cterm list -> thm -> thm
+  val IT_EXISTS: (cterm*cterm) list -> thm -> thm
 
-  val EVEN_ORS : thm list -> thm list
-  val DISJ_CASESL : thm -> thm list -> thm
+  val EVEN_ORS: thm list -> thm list
+  val DISJ_CASESL: thm -> thm list -> thm
 
-  val list_beta_conv : cterm -> cterm list -> thm
-  val SUBS : thm list -> thm -> thm
-  val simpl_conv : simpset -> thm list -> cterm -> thm
+  val list_beta_conv: cterm -> cterm list -> thm
+  val SUBS: thm list -> thm -> thm
+  val simpl_conv: simpset -> thm list -> cterm -> thm
 
-  val rbeta : thm -> thm
+  val rbeta: thm -> thm
 (* For debugging my isabelle solver in the conditional rewriter *)
-  val term_ref : term list ref
-  val thm_ref : thm list ref
-  val ss_ref : simpset list ref
-  val tracing : bool ref
-  val CONTEXT_REWRITE_RULE : term * term list * thm * thm list
+  val term_ref: term list ref
+  val thm_ref: thm list ref
+  val ss_ref: simpset list ref
+  val tracing: bool ref
+  val CONTEXT_REWRITE_RULE: term * term list * thm * thm list
                              -> thm -> thm * term list
-  val RIGHT_ASSOC : thm -> thm
+  val RIGHT_ASSOC: thm -> thm
 
-  val prove : bool -> cterm * tactic -> thm
+  val prove: bool -> cterm * tactic -> thm
 end;
 
 structure Rules: RULES =
@@ -308,7 +308,7 @@
    let val gth = forall_intr v th
        val {prop=Const("all",_)$Abs(x,ty,rst),sign,...} = rep_thm gth
        val P' = Abs(x,ty, HOLogic.dest_Trueprop rst)  (* get rid of trueprop *)
-       val theta = Pattern.match sign (P,P')
+       val theta = Pattern.match sign (P,P') (Vartab.empty, Vartab.empty);
        val allI2 = instantiate (certify sign theta) allI
        val thm = Thm.implies_elim allI2 gth
        val {prop = tp $ (A $ Abs(_,_,M)),sign,...} = rep_thm thm
@@ -353,7 +353,7 @@
     val lam = #2 (D.dest_comb (D.drop_prop (cconcl exth)))
     val redex = D.capply lam fvar
     val {sign, t = t$u,...} = Thm.rep_cterm redex
-    val residue = Thm.cterm_of sign (betapply (t, u))
+    val residue = Thm.cterm_of sign (Term.betapply (t, u))
   in
     GEN fvar (DISCH residue fact) RS (exth RS Thms.choose_thm)
       handle THM (msg, _, _) => raise RULES_ERR "CHOOSE" msg
diff -r a9f67248996a -r 43c4589a9a78 TFL/thry.ML
--- a/TFL/thry.ML	Wed Nov 16 17:45:29 2005 +0100
+++ b/TFL/thry.ML	Wed Nov 16 17:45:30 2005 +0100
@@ -34,7 +34,7 @@
 
 fun match_term thry pat ob =
   let
-    val (ty_theta, tm_theta) = Pattern.match thry (pat,ob)
+    val (ty_theta, tm_theta) = Pattern.match thry (pat,ob) (Vartab.empty, Vartab.empty);
     fun tmbind (ixn, (T, t)) = (Var (ixn, Envir.typ_subst_TVars ty_theta T), t)
   in (map tmbind (Vartab.dest tm_theta), map tybind (Vartab.dest ty_theta))
   end;
diff -r a9f67248996a -r 43c4589a9a78 src/Pure/IsaPlanner/term_lib.ML
--- a/src/Pure/IsaPlanner/term_lib.ML	Wed Nov 16 17:45:29 2005 +0100
+++ b/src/Pure/IsaPlanner/term_lib.ML	Wed Nov 16 17:45:30 2005 +0100
@@ -141,7 +141,7 @@
 (* Higher order matching with exception handled *)
 (* returns optional instantiation *)
 fun clean_match thy (a as (pat, t)) =
-  let val (tyenv, tenv) = Pattern.match thy a
+  let val (tyenv, tenv) = Pattern.match thy a (Vartab.empty, Vartab.empty)
   in SOME (Vartab.dest tyenv, Vartab.dest tenv)
   end handle Pattern.MATCH => NONE;
 (* Higher order unification with exception handled, return the instantiations *)
diff -r a9f67248996a -r 43c4589a9a78 src/Pure/Isar/find_theorems.ML
--- a/src/Pure/Isar/find_theorems.ML	Wed Nov 16 17:45:29 2005 +0100
+++ b/src/Pure/Isar/find_theorems.ML	Wed Nov 16 17:45:30 2005 +0100
@@ -83,7 +83,8 @@
       Pattern.matches thy (if po then (pat, obj) else (obj, pat));
 
     fun substsize pat =
-      let val (_, subst) = Pattern.match thy (if po then (pat, obj) else (obj, pat))
+      let val (_, subst) =
+        Pattern.match thy (if po then (pat, obj) else (obj, pat)) (Vartab.empty, Vartab.empty)
       in Vartab.fold (fn (_, (_, t)) => fn n => size_of_term t + n) subst 0 end;
 
     fun bestmatch [] = NONE
diff -r a9f67248996a -r 43c4589a9a78 src/Pure/Proof/extraction.ML
--- a/src/Pure/Proof/extraction.ML	Wed Nov 16 17:45:29 2005 +0100
+++ b/src/Pure/Proof/extraction.ML	Wed Nov 16 17:45:30 2005 +0100
@@ -103,14 +103,13 @@
         let
           fun ren t = getOpt (Term.rename_abs tm1 tm t, t);
           val inc = Logic.incr_indexes ([], maxidx_of_term tm + 1);
-          val env as (Tenv, tenv) = Pattern.match thy (inc tm1, tm);
+          val env as (Tenv, tenv) = Pattern.match thy (inc tm1, tm) (Vartab.empty, Vartab.empty);
           val prems' = map (pairself (Envir.subst_vars env o inc o ren)) prems;
           val env' = Envir.Envir
             {maxidx = Library.foldl Int.max
               (~1, map (Int.max o pairself maxidx_of_term) prems'),
              iTs = Tenv, asol = tenv};
-          val env'' = Library.foldl (fn (env, p) =>
-            Pattern.unify (thy, env, [pairself (lookup rew) p])) (env', prems')
+          val env'' = fold (Pattern.unify 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)
diff -r a9f67248996a -r 43c4589a9a78 src/Pure/Proof/reconstruct.ML
--- a/src/Pure/Proof/reconstruct.ML	Wed Nov 16 17:45:29 2005 +0100
+++ b/src/Pure/Proof/reconstruct.ML	Wed Nov 16 17:45:30 2005 +0100
@@ -132,7 +132,7 @@
         val t' = mk_abs Ts t;
         val u' = mk_abs Ts u
       in
-        (prop, prf, cs, Pattern.unify (sg, env, [(t', u')]), vTs)
+        (prop, prf, cs, Pattern.unify sg (t', u') env, vTs)
         handle Pattern.Pattern =>
             let val (env', cs') = decompose sg [] (env, (t', u'))
             in (prop, prf, cs @ cs', env', vTs) end
@@ -268,8 +268,8 @@
                   val tn2 = Envir.norm_term bigenv t2
                 in
                   if Pattern.pattern tn1 andalso Pattern.pattern tn2 then
-                    ((Pattern.unify (sg, env, [(tn1, tn2)]), ps) handle Pattern.Unif =>
-                       cantunify sg (tn1, tn2))
+                    (Pattern.unify sg (tn1, tn2) env, ps) handle Pattern.Unif =>
+                       cantunify sg (tn1, tn2)
                   else
                     let val (env', cs') = decompose sg [] (env, (tn1, tn2))
                     in if cs' = [(tn1, tn2)] then
diff -r a9f67248996a -r 43c4589a9a78 src/Pure/thm.ML
--- a/src/Pure/thm.ML	Wed Nov 16 17:45:29 2005 +0100
+++ b/src/Pure/thm.ML	Wed Nov 16 17:45:30 2005 +0100
@@ -292,7 +292,7 @@
      ct2 as Cterm {t = t2, maxidx = maxidx2, sorts = sorts2, ...}) =
   let
     val thy_ref = merge_thys0 ct1 ct2;
-    val (Tinsts, tinsts) = match (Theory.deref thy_ref) (t1, t2);
+    val (Tinsts, tinsts) = match (Theory.deref thy_ref) (t1, t2) (Vartab.empty, Vartab.empty);
     val maxidx = Int.max (maxidx1, maxidx2);
     val sorts = Sorts.union sorts1 sorts2;
     fun mk_cTinst (ixn, (S, T)) =
diff -r a9f67248996a -r 43c4589a9a78 src/Pure/unify.ML
--- a/src/Pure/unify.ML	Wed Nov 16 17:45:29 2005 +0100
+++ b/src/Pure/unify.ML	Wed Nov 16 17:45:30 2005 +0100
@@ -588,8 +588,8 @@
      val dps = map (fn(t,u)=> ([],t,u)) tus
   in add_unify 1 ((env, dps), Seq.empty) end;
 
-fun unifiers params =
-  Seq.cons ((Pattern.unify params, []), Seq.empty)
+fun unifiers (params as (thy, env, tus)) =
+  Seq.cons ((fold (Pattern.unify thy) tus env, []), Seq.empty)
     handle Pattern.Unif => Seq.empty
          | Pattern.Pattern => hounifiers params;