# HG changeset patch
# User wenzelm
# Date 1150139940 -7200
# Node ID 620d90091788fb8d1089bed4ba8e8ab0ce9b3247
# Parent  6e44610bdd761f5bf56720c9670a728e7fd738b0
tuned Seq/Envir/Unify interfaces;

diff -r 6e44610bdd76 -r 620d90091788 src/HOL/TLA/Intensional.ML
--- a/src/HOL/TLA/Intensional.ML	Mon Jun 12 21:18:10 2006 +0200
+++ b/src/HOL/TLA/Intensional.ML	Mon Jun 12 21:19:00 2006 +0200
@@ -89,7 +89,7 @@
   let
     (* analogous to RS, but using matching instead of resolution *)
     fun matchres tha i thb =
-      case Seq.chop (2, biresolution true [(false,tha)] i thb) of
+      case Seq.chop 2 (biresolution true [(false,tha)] i thb) of
           ([th],_) => th
         | ([],_)   => raise THM("matchres: no match", i, [tha,thb])
         |      _   => raise THM("matchres: multiple unifiers", i, [tha,thb])
diff -r 6e44610bdd76 -r 620d90091788 src/HOL/Tools/inductive_codegen.ML
--- a/src/HOL/Tools/inductive_codegen.ML	Mon Jun 12 21:18:10 2006 +0200
+++ b/src/HOL/Tools/inductive_codegen.ML	Mon Jun 12 21:19:00 2006 +0200
@@ -225,7 +225,7 @@
 datatype indprem = Prem of term list * term | Sidecond of term;
 
 fun select_mode_prem thy modes vs ps =
-  find_first (isSome o snd) (ps ~~ map
+  find_first (is_some o snd) (ps ~~ map
     (fn Prem (us, t) => find_first (fn Mode ((_, is), _) =>
           let
             val (in_ts, out_ts) = get_args is 1 us;
@@ -574,7 +574,7 @@
              [(split_prod [] ((the o AList.lookup (op =) factors) name) t, prems)]) clauses
         end;
 
-      fun check_set (Const (s, _)) = s mem names orelse isSome (get_clauses thy s)
+      fun check_set (Const (s, _)) = s mem names orelse is_some (get_clauses thy s)
         | check_set (Var ((s, _), _)) = s mem arg_vs
         | check_set _ = false;
 
@@ -746,13 +746,13 @@
 infix 5 :->;
 infix 3 ++;
 
-fun s :-> f = Seq.flat (Seq.map f s);
+fun s :-> f = Seq.maps f s;
 
-fun s1 ++ s2 = Seq.append (s1, s2);
+fun s1 ++ s2 = Seq.append s1 s2;
 
 fun ?? b = if b then Seq.single () else Seq.empty;
 
-fun ?! s = isSome (Seq.pull s);    
+fun ?! s = is_some (Seq.pull s);
 
 fun equal__1 x = Seq.single x;
 
diff -r 6e44610bdd76 -r 620d90091788 src/Provers/IsaPlanner/isand.ML
--- a/src/Provers/IsaPlanner/isand.ML	Mon Jun 12 21:18:10 2006 +0200
+++ b/src/Provers/IsaPlanner/isand.ML	Mon Jun 12 21:19:00 2006 +0200
@@ -124,8 +124,7 @@
 fun solve_with sol th = 
     let fun solvei 0 = Seq.empty
           | solvei i = 
-            Seq.append (bicompose false (false,sol,0) i th, 
-                        solvei (i - 1))
+            Seq.append (bicompose false (false,sol,0) i th) (solvei (i - 1))
     in
       solvei (Thm.nprems_of th)
     end;
diff -r 6e44610bdd76 -r 620d90091788 src/Provers/IsaPlanner/zipper.ML
--- a/src/Provers/IsaPlanner/zipper.ML	Mon Jun 12 21:18:10 2006 +0200
+++ b/src/Provers/IsaPlanner/zipper.ML	Mon Jun 12 21:19:00 2006 +0200
@@ -321,7 +321,7 @@
             (case lzy z
               of NONE => NONE
                | SOME (hz,mz) => 
-                 SOME (hz, Seq.append (mz, Seq.make (lzyl more))))
+                 SOME (hz, Seq.append mz (Seq.make (lzyl more))))
         and lzy z = lzyl (fsearch z) ()
       in Seq.make o lzyl o fsearch end;
 
@@ -335,7 +335,7 @@
           | lzyl a ((LookIn z) :: more) () =
             (case lzy a z
               of NONE => lzyl a more ()
-               | SOME(hz,mz) => SOME(hz,Seq.append(mz,Seq.make(lzyl a more))))
+               | SOME(hz,mz) => SOME(hz,Seq.append mz (Seq.make(lzyl a more))))
         and lzy a z = 
             let val (a2, slist) = (fsearch a z) in lzyl a2 slist () end
 
@@ -351,7 +351,7 @@
           | lzyl ((a, LookIn z) :: more) () =
             (case lzyl (fsearch a z) () of 
                NONE => lzyl more ()
-             | SOME (z,mz) => SOME (z,Seq.append(mz, Seq.make (lzyl more))))
+             | SOME (z,mz) => SOME (z,Seq.append mz (Seq.make (lzyl more))))
       in Seq.make (lzyl (fsearch a0 z)) end;
 
 
diff -r 6e44610bdd76 -r 620d90091788 src/Provers/eqsubst.ML
--- a/src/Provers/eqsubst.ML	Mon Jun 12 21:18:10 2006 +0200
+++ b/src/Provers/eqsubst.ML	Mon Jun 12 21:19:00 2006 +0200
@@ -125,7 +125,7 @@
              Envir.alist_of env);
           val initenv = Envir.Envir {asol = Vartab.empty,
                                      iTs = typinsttab, maxidx = ix2};
-          val useq = (Unify.smash_unifiers (sgn,initenv,[a]))
+          val useq = Unify.smash_unifiers sgn [a] initenv
 	            handle UnequalLengths => Seq.empty
 		               | Term.TERM _ => Seq.empty;
           fun clean_unify' useq () =
@@ -380,9 +380,8 @@
                 (case searchf searchinfo occ lhs of
                    SkipMore i => occ_search i moreasms
                  | SkipSeq ss =>
-                   Seq.append (Seq.map (Library.pair asminfo)
-                                       (Seq.flat ss),
-                               occ_search 1 moreasms))
+                   Seq.append (Seq.map (Library.pair asminfo) (Seq.flat ss))
+                               (occ_search 1 moreasms))
                               (* find later substs also *)
           in
             occ_search skipocc asmpreps |> Seq.maps (apply_subst_in_asm i th r)
diff -r 6e44610bdd76 -r 620d90091788 src/Provers/induct_method.ML
--- a/src/Provers/induct_method.ML	Mon Jun 12 21:18:10 2006 +0200
+++ b/src/Provers/induct_method.ML	Mon Jun 12 21:19:00 2006 +0200
@@ -228,8 +228,8 @@
         val rule' = Thm.incr_indexes (maxidx + 1) rule;
         val concl = Logic.strip_assums_concl goal;
       in
-        Unify.smash_unifiers (thy, Envir.empty (#maxidx (Thm.rep_thm rule')),
-          [(Thm.concl_of rule', concl)])
+        Unify.smash_unifiers thy [(Thm.concl_of rule', concl)]
+          (Envir.empty (#maxidx (Thm.rep_thm rule')))
         |> Seq.map (fn env => Drule.instantiate (dest_env thy env) rule')
       end
   end handle Subscript => Seq.empty;
diff -r 6e44610bdd76 -r 620d90091788 src/Pure/Isar/calculation.ML
--- a/src/Pure/Isar/calculation.ML	Mon Jun 12 21:18:10 2006 +0200
+++ b/src/Pure/Isar/calculation.ML	Mon Jun 12 21:19:00 2006 +0200
@@ -84,7 +84,7 @@
 (* symmetric *)
 
 val symmetric = Thm.rule_attribute (fn x => fn th =>
-  (case Seq.chop (2, Drule.multi_resolves [th] (#2 (#1 (CalculationData.get x)))) of
+  (case Seq.chop 2 (Drule.multi_resolves [th] (#2 (#1 (CalculationData.get x)))) of
     ([th'], _) => th'
   | ([], _) => raise THM ("symmetric: no unifiers", 1, [th])
   | _ => raise THM ("symmetric: multiple unifiers", 1, [th])));
diff -r 6e44610bdd76 -r 620d90091788 src/Pure/drule.ML
--- a/src/Pure/drule.ML	Mon Jun 12 21:18:10 2006 +0200
+++ b/src/Pure/drule.ML	Mon Jun 12 21:19:00 2006 +0200
@@ -434,7 +434,7 @@
   This step can lose information.*)
 fun flexflex_unique th =
   if null (tpairs_of th) then th else
-    case Seq.chop (2, flexflex_rule th) of
+    case Seq.chop 2 (flexflex_rule th) of
       ([th],_) => th
     | ([],_)   => raise THM("flexflex_unique: impossible constraints", 0, [th])
     |      _   => raise THM("flexflex_unique: multiple unifiers", 0, [th]);
@@ -538,7 +538,7 @@
 
 (*Resolution: exactly one resolvent must be produced.*)
 fun tha RSN (i,thb) =
-  case Seq.chop (2, biresolution false [(false,tha)] i thb) of
+  case Seq.chop 2 (biresolution false [(false,tha)] i thb) of
       ([th],_) => th
     | ([],_)   => raise THM("RSN: no unifiers", i, [tha,thb])
     |      _   => raise THM("RSN: multiple unifiers", i, [tha,thb]);
diff -r 6e44610bdd76 -r 620d90091788 src/Pure/envir.ML
--- a/src/Pure/envir.ML	Mon Jun 12 21:18:10 2006 +0200
+++ b/src/Pure/envir.ML	Mon Jun 12 21:19:00 2006 +0200
@@ -21,7 +21,7 @@
   val update: ((indexname * typ) * term) * env -> env
   val empty: int -> env
   val is_empty: env -> bool
-  val above: int * env -> bool
+  val above: env -> int -> bool
   val vupdate: ((indexname * typ) * term) * env -> env
   val alist_of: env -> (indexname * (typ * term)) list
   val norm_term: env -> term -> term
@@ -104,12 +104,9 @@
 fun is_empty (Envir {asol, iTs, ...}) = Vartab.is_empty asol andalso Vartab.is_empty iTs;
 
 (*Determine if the least index updated exceeds lim*)
-fun above (lim, Envir {asol, iTs, ...}) =
-  (case (Vartab.min_key asol, Vartab.min_key iTs) of
-     (NONE, NONE) => true
-   | (SOME (_, i), NONE) => i > lim
-   | (NONE, SOME (_, i')) => i' > lim
-   | (SOME (_, i), SOME (_, i')) => i > lim andalso i' > lim);
+fun above (Envir {asol, iTs, ...}) lim =
+  (case Vartab.min_key asol of SOME (_, i) => i > lim | NONE => true) andalso
+  (case Vartab.min_key iTs of SOME (_, i) => i > lim | NONE => true);
 
 (*Update, checking Var-Var assignments: try to suppress higher indexes*)
 fun vupdate ((aU as (a, U), t), env as Envir {iTs, ...}) = case t of
diff -r 6e44610bdd76 -r 620d90091788 src/Pure/tctical.ML
--- a/src/Pure/tctical.ML	Mon Jun 12 21:18:10 2006 +0200
+++ b/src/Pure/tctical.ML	Mon Jun 12 21:19:00 2006 +0200
@@ -102,8 +102,7 @@
   Like ORELSE, but allows backtracking on both tac1 and tac2.
   The tactic tac2 is not applied until needed.*)
 fun (tac1 APPEND tac2) st =
-  Seq.append(tac1 st,
-                  Seq.make(fn()=> Seq.pull (tac2 st)));
+  Seq.append (tac1 st) (Seq.make(fn()=> Seq.pull (tac2 st)));
 
 (*Like APPEND, but interleaves results of tac1 and tac2.*)
 fun (tac1 INTLEAVE tac2) st =
diff -r 6e44610bdd76 -r 620d90091788 src/Pure/thm.ML
--- a/src/Pure/thm.ML	Mon Jun 12 21:18:10 2006 +0200
+++ b/src/Pure/thm.ML	Mon Jun 12 21:19:00 2006 +0200
@@ -951,7 +951,7 @@
   Resulting sequence may contain multiple elements if the tpairs are
     not all flex-flex. *)
 fun flexflex_rule (th as Thm {thy_ref, der, maxidx, shyps, hyps, tpairs, prop}) =
-  Unify.smash_unifiers (Theory.deref thy_ref, Envir.empty maxidx, tpairs)
+  Unify.smash_unifiers (Theory.deref thy_ref) tpairs (Envir.empty maxidx)
   |> Seq.map (fn env =>
       if Envir.is_empty env then th
       else
@@ -1426,7 +1426,7 @@
              if Envir.is_empty env then (tpairs, (Bs @ As, C))
              else
              let val ntps = map (pairself normt) tpairs
-             in if Envir.above (smax, env) then
+             in if Envir.above env smax then
                   (*no assignments in state; normalize the rule only*)
                   if lifted
                   then (ntps, (Bs @ map (norm_term_skip env nlift) As, C))
@@ -1439,7 +1439,7 @@
              Thm{thy_ref = thy_ref,
                  der = Pt.infer_derivs
                    ((if Envir.is_empty env then I
-                     else if Envir.above (smax, env) then
+                     else if Envir.above env smax then
                        (fn f => fn der => f (Pt.norm_proof' env der))
                      else
                        curry op oo (Pt.norm_proof' env))