# HG changeset patch
# User paulson
# Date 856535507 -3600
# Node ID 85d7e800d7548f959922564ac29f6f28c2ffdd24
# Parent  510d94c71dda433bb7def920cbf77db1f610767b
Replaced "flat" by the Basis Library function List.concat

diff -r 510d94c71dda -r 85d7e800d754 src/Pure/axclass.ML
--- a/src/Pure/axclass.ML	Fri Feb 21 15:30:41 1997 +0100
+++ b/src/Pure/axclass.ML	Fri Feb 21 15:31:47 1997 +0100
@@ -199,7 +199,7 @@
           else err_bad_axsort name class
       | _ => err_bad_tfrees name);
 
-    val axS = Sign.norm_sort sign (logicC :: flat (map axm_sort axioms));
+    val axS = Sign.norm_sort sign (logicC :: List.concat(map axm_sort axioms))
 
     val int_axm = Logic.close_form o map_term_tfrees (K (aT axS));
     fun inclass c = Logic.mk_inclass (aT axS, c);
diff -r 510d94c71dda -r 85d7e800d754 src/Pure/deriv.ML
--- a/src/Pure/deriv.ML	Fri Feb 21 15:30:41 1997 +0100
+++ b/src/Pure/deriv.ML	Fri Feb 21 15:31:47 1997 +0100
@@ -38,7 +38,7 @@
 	Join (Bicompose arg, linear rder) :: rev_deriv sder
   | rev_deriv (Join (_, [der]))	= rev_deriv der
   | rev_deriv (Join (rl, der::ders)) =	(*catch-all case; doubtful?*)
-        Join(rl, flat (map linear ders)) :: rev_deriv der
+        Join(rl, List.concat (map linear ders)) :: rev_deriv der
 and linear der 	= rev (rev_deriv der);
 
 
diff -r 510d94c71dda -r 85d7e800d754 src/Pure/drule.ML
--- a/src/Pure/drule.ML	Fri Feb 21 15:30:41 1997 +0100
+++ b/src/Pure/drule.ML	Fri Feb 21 15:31:47 1997 +0100
@@ -80,10 +80,10 @@
 (*results may contain duplicates!*)
 
 fun ancestry_of thy =
-  thy :: flat (map ancestry_of (parents_of thy));
+  thy :: List.concat (map ancestry_of (parents_of thy));
 
 val all_axioms_of =
-  flat o map (Symtab.dest o #new_axioms o rep_theory) o ancestry_of;
+  List.concat o map (Symtab.dest o #new_axioms o rep_theory) o ancestry_of;
 
 
 (* clash_types, clash_consts *)
@@ -389,7 +389,7 @@
 fun thas RLN (i,thbs) =
   let val resolve = biresolution false (map (pair false) thas) i
       fun resb thb = Sequence.list_of_s (resolve thb) handle THM _ => []
-  in  flat (map resb thbs)  end;
+  in  List.concat (map resb thbs)  end;
 
 fun thas RL thbs = thas RLN (1,thbs);
 
diff -r 510d94c71dda -r 85d7e800d754 src/Pure/net.ML
--- a/src/Pure/net.ML	Fri Feb 21 15:30:41 1997 +0100
+++ b/src/Pure/net.ML	Fri Feb 21 15:31:47 1997 +0100
@@ -203,7 +203,7 @@
 	     | _ => rands t (net, var::nets)	(*var could match also*)
   end;
 
-fun extract_leaves l = flat (map (fn Leaf(xs) => xs) l);
+fun extract_leaves l = List.concat (map (fn Leaf(xs) => xs) l);
 
 (*return items whose key could match t, WHICH MUST BE BETA-ETA NORMAL*)
 fun match_term net t = 
diff -r 510d94c71dda -r 85d7e800d754 src/Pure/search.ML
--- a/src/Pure/search.ML	Fri Feb 21 15:30:41 1997 +0100
+++ b/src/Pure/search.ML	Fri Feb 21 15:31:47 1997 +0100
@@ -5,8 +5,13 @@
 Search tacticals
 *)
 
+infix 1 THEN_MAYBE THEN_MAYBE';
+
 signature SEARCH =
   sig
+  val THEN_MAYBE	: tactic * tactic -> tactic
+  val THEN_MAYBE'	: ('a -> tactic) * ('a -> tactic) -> ('a -> tactic)
+
   val trace_DEPTH_FIRST	: bool ref
   val DEPTH_FIRST	: (thm -> bool) -> tactic -> tactic
   val DEPTH_SOLVE	: tactic -> tactic
@@ -57,6 +62,14 @@
 (*Apply a tactic if subgoals remain, else do nothing.*)
 val IF_UNSOLVED = COND (has_fewer_prems 1) all_tac;
 
+(*Execute tac1, but only execute tac2 if there are at least as many subgoals
+  as before.  This ensures that tac2 is only applied to an outcome of tac1.*)
+fun tac1 THEN_MAYBE tac2 = STATE
+    (fn st => tac1  THEN  
+	 COND (has_fewer_prems (nprems_of st)) all_tac tac2);
+
+fun (tac1 THEN_MAYBE' tac2) x = tac1 x THEN_MAYBE tac2 x;
+
 (*Tactical to reduce the number of premises by 1.
   If no subgoals then it must fail! *)
 fun DEPTH_SOLVE_1 tac = STATE
@@ -198,7 +211,7 @@
 	      ([],[]) => []
 	    | ([],nonsats) => 
 		  (prs("breadth=" ^ string_of_int(length nonsats) ^ "\n");
-		   bfs (flat (map tacf nonsats)))
+		   bfs (List.concat (map tacf nonsats)))
 	    | (sats,_)  => sats)
   in (fn st => Sequence.s_of_list (bfs [st])) end;
 
diff -r 510d94c71dda -r 85d7e800d754 src/Pure/sign.ML
--- a/src/Pure/sign.ML	Fri Feb 21 15:30:41 1997 +0100
+++ b/src/Pure/sign.ML	Fri Feb 21 15:31:47 1997 +0100
@@ -197,7 +197,7 @@
     Pretty.writeln (Pretty.big_list "types:" (map pretty_ty tycons));
     Pretty.writeln (Pretty.big_list "abbrs:" (map (pretty_abbr syn) abbrs));
     Pretty.writeln (Pretty.big_list "arities:"
-                      (flat (map pretty_arities arities)));
+                      (List.concat (map pretty_arities arities)));
     Pretty.writeln (Pretty.big_list "consts:"
                       (map (pretty_const syn) (Symtab.dest const_tab)))
   end;
diff -r 510d94c71dda -r 85d7e800d754 src/Pure/symtab.ML
--- a/src/Pure/symtab.ML	Fri Feb 21 15:30:41 1997 +0100
+++ b/src/Pure/symtab.ML	Fri Feb 21 15:31:47 1997 +0100
@@ -157,7 +157,7 @@
   balance (foldr cons_entry (alst, Tip));
 
 fun dest_multi tab =
-  flat (map (fn (key, entries) => map (pair key) entries) (dest tab));
+  List.concat (map (fn (key, entries) => map (pair key) entries) (dest tab));
 
 
 (* map tables *)
diff -r 510d94c71dda -r 85d7e800d754 src/Pure/tactic.ML
--- a/src/Pure/tactic.ML	Fri Feb 21 15:30:41 1997 +0100
+++ b/src/Pure/tactic.ML	Fri Feb 21 15:31:47 1997 +0100
@@ -61,6 +61,7 @@
   val net_biresolve_tac: (bool*thm) list -> int -> tactic
   val net_match_tac: thm list -> int -> tactic
   val net_resolve_tac: thm list -> int -> tactic
+  val orderlist: (int * 'a) list -> 'a list
   val PRIMITIVE: (thm -> thm) -> tactic  
   val PRIMSEQ: (thm -> thm Sequence.seq) -> tactic  
   val prune_params_tac: tactic
@@ -387,7 +388,7 @@
       let val hyps = Logic.strip_assums_hyp prem
           and concl = Logic.strip_assums_concl prem 
           val kbrls = Net.unify_term inet concl @
-                      flat (map (Net.unify_term enet) hyps)
+                      List.concat (map (Net.unify_term enet) hyps)
       in PRIMSEQ (biresolution match (orderlist kbrls) i) end);
 
 (*versions taking pre-built nets*)
@@ -527,11 +528,8 @@
 
 (*rotate_tac n i: rotate the assumptions of subgoal i by n positions, from
   right to left if n is positive, and from left to right if n is negative.*)
-fun rotate_tac n =
-  let fun rot(n) = EVERY'(replicate n (dtac asm_rl));
-  in if n >= 0 then rot n
-     else SUBGOAL (fn (t,i) => rot(length(Logic.strip_assums_hyp t)+n) i)
-  end;
+fun rotate_tac 0 i = all_tac
+  | rotate_tac k i = PRIMITIVE (rotate_rule k i);
 
 end;
 
diff -r 510d94c71dda -r 85d7e800d754 src/Pure/tctical.ML
--- a/src/Pure/tctical.ML	Fri Feb 21 15:30:41 1997 +0100
+++ b/src/Pure/tctical.ML	Fri Feb 21 15:31:47 1997 +0100
@@ -6,7 +6,7 @@
 Tacticals
 *)
 
-infix 1 THEN THEN' THEN_MAYBE THEN_MAYBE';
+infix 1 THEN THEN';
 infix 0 ORELSE APPEND INTLEAVE ORELSE' APPEND' INTLEAVE';
 infix 0 THEN_ELSE;
 
@@ -55,8 +55,6 @@
   val suppress_tracing  : bool ref
   val THEN              : tactic * tactic -> tactic
   val THEN'             : ('a -> tactic) * ('a -> tactic) -> 'a -> tactic
-  val THEN_MAYBE	: tactic * tactic -> tactic
-  val THEN_MAYBE'	: ('a -> tactic) * ('a -> tactic) -> ('a -> tactic)
   val THEN_ELSE         : tactic * (tactic*tactic) -> tactic
   val traced_tac        : (thm -> (thm * thm Sequence.seq) option) -> tactic
   val tracify           : bool ref -> tactic -> thm -> thm Sequence.seq
@@ -148,21 +146,34 @@
 (*Do the tactic or else do nothing*)
 fun TRY tac = tac ORELSE all_tac;
 
-(*Execute tac1, but only execute tac2 if there are at least as many subgoals
-  as before.  This ensures that tac2 is only applied to an outcome of tac1.*)
-fun tac1 THEN_MAYBE tac2 = let fun has_fewer_prems n rule = (nprems_of rule < n)
-in STATE (fn state => tac1  THEN  
-	 COND (has_fewer_prems (nprems_of state)) all_tac tac2) end;
-fun (tac1 THEN_MAYBE' tac2) x = tac1 x THEN_MAYBE tac2 x;
+(*** List-oriented tactics ***)
+
+local
+  (*This version of EVERY avoids backtracking over repeated states*)
+
+  fun EVY (trail, []) st = 
+	Sequence.seqof (fn()=> Some(st, 
+			Sequence.seqof (fn()=> Sequence.pull (evyBack trail))))
+    | EVY (trail, tac::tacs) st = 
+	  case Sequence.pull(tac st) of
+	      None    => evyBack trail              (*failed: backtrack*)
+	    | Some(st',q) => EVY ((st',q,tacs)::trail, tacs) st'
+  and evyBack [] = Sequence.null (*no alternatives*)
+    | evyBack ((st',q,tacs)::trail) =
+	  case Sequence.pull q of
+	      None        => evyBack trail
+	    | Some(st,q') => if eq_thm (st',st) 
+			     then evyBack ((st',q',tacs)::trail)
+			     else EVY ((st,q',tacs)::trail, tacs) st
+in
+
+(* EVERY [tac1,...,tacn]   equals    tac1 THEN ... THEN tacn   *)
+fun EVERY tacs = EVY ([], tacs);
+end;
 
 
-(*** List-oriented tactics ***)
-
-(* EVERY [tac1,...,tacn]   equals    tac1 THEN ... THEN tacn   *)
-fun EVERY tacs = foldr (op THEN) (tacs, all_tac);
-
 (* EVERY' [tac1,...,tacn] i  equals    tac1 i THEN ... THEN tacn i   *)
-fun EVERY' tacs = foldr (op THEN') (tacs, K all_tac);
+fun EVERY' tacs i = EVERY (map (fn f => f i) tacs);
 
 (*Apply every tactic to 1*)
 fun EVERY1 tacs = EVERY' tacs 1;
diff -r 510d94c71dda -r 85d7e800d754 src/Pure/type.ML
--- a/src/Pure/type.ML	Fri Feb 21 15:30:41 1997 +0100
+++ b/src/Pure/type.ML	Fri Feb 21 15:31:47 1997 +0100
@@ -758,7 +758,8 @@
   let
     val TySg {classes, subclass, default, tycons, arities, abbrs} = tsig;
     val arities1 =
-      flat (map (fn (t, ss, cs) => map (fn c => (t, (ss, c))) cs) sarities);
+      List.concat 
+          (map (fn (t, ss, cs) => map (fn c => (t, (ss, c))) cs) sarities);
     val arities2 = foldl (coregular (classes, subclass, tycons))
                          (arities, min_domain subclass arities1)
       |> close subclass;