--- 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])
--- 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;
--- 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;
--- 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;
--- 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)
--- 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;
--- 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])));
--- 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]);
--- 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
--- 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 =
--- 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))