src/FOLP/simp.ML

--- a/src/FOLP/simp.ML	Thu Mar 03 09:22:35 2005 +0100
+++ b/src/FOLP/simp.ML	Thu Mar 03 12:43:01 2005 +0100
@@ -84,7 +84,7 @@
           biresolve_tac (Net.unify_term net
                        (lhs_of (strip_assums_concl prem))) i);
 
-fun nth_subgoal i thm = nth_elem(i-1,prems_of thm);
+fun nth_subgoal i thm = List.nth(prems_of thm,i-1);
 
 fun goal_concl i thm = strip_assums_concl(nth_subgoal i thm);
 
@@ -161,7 +161,7 @@
                      in case f of
                             Const(c,T) => 
                                 if c mem ccs
-                                then foldr add_hvars (args,hvars)
+                                then Library.foldr add_hvars (args,hvars)
                                 else add_term_vars(tm,hvars)
                           | _ => add_term_vars(tm,hvars)
                      end
@@ -173,7 +173,7 @@
                 if at then vars else add_term_vars(tm,vars)
         fun add_list(tm,al,vars) = let val (_,tml) = strip_comb tm
                 in if length(tml)=length(al)
-                   then foldr itf (tml~~al,vars)
+                   then Library.foldr itf (tml~~al,vars)
                    else vars
                 end
         fun add_vars (tm,vars) = case tm of
@@ -194,12 +194,12 @@
     val lhs = rhs_of_eq 1 thm'
     val rhs = lhs_of_eq nops thm'
     val asms = tl(rev(tl(prems_of thm')))
-    val hvars = foldr (add_hidden_vars ccs) (lhs::rhs::asms,[])
+    val hvars = Library.foldr (add_hidden_vars ccs) (lhs::rhs::asms,[])
     val hvars = add_new_asm_vars new_asms (rhs,hvars)
     fun it_asms (asm,hvars) =
         if atomic asm then add_new_asm_vars new_asms (asm,hvars)
         else add_term_frees(asm,hvars)
-    val hvars = foldr it_asms (asms,hvars)
+    val hvars = Library.foldr it_asms (asms,hvars)
     val hvs = map (#1 o dest_Var) hvars
     val refl1_tac = refl_tac 1
     fun norm_step_tac st = st |>
@@ -216,7 +216,7 @@
 
 fun add_norm_tags congs =
     let val ccs = map cong_const congs
-        val new_asms = filter (exists not o #2)
+        val new_asms = List.filter (exists not o #2)
                 (ccs ~~ (map (map atomic o prems_of) congs));
     in add_norms(congs,ccs,new_asms) end;
 
@@ -252,7 +252,7 @@
     (writeln"\nDuplicate rewrite or congruence rule:"; print_thm th;
      net);
 
-val insert_thms = foldr insert_thm_warn;
+val insert_thms = Library.foldr insert_thm_warn;
 
 fun addrew(SS{auto_tac,congs,cong_net,mk_simps,simps,simp_net}, thm) =
 let val thms = mk_simps thm
@@ -260,7 +260,7 @@
       simps = (thm,thms)::simps, simp_net = insert_thms(thms,simp_net)}
 end;
 
-val op addrews = foldl addrew;
+val op addrews = Library.foldl addrew;
 
 fun op addcongs(SS{auto_tac,congs,cong_net,mk_simps,simps,simp_net}, thms) =
 let val congs' = thms @ congs;
@@ -278,10 +278,10 @@
     (writeln"\nNo such rewrite or congruence rule:";  print_thm th;
      net);
 
-val delete_thms = foldr delete_thm_warn;
+val delete_thms = Library.foldr delete_thm_warn;
 
 fun op delcongs(SS{auto_tac,congs,cong_net,mk_simps,simps,simp_net}, thms) =
-let val congs' = foldl (gen_rem Drule.eq_thm_prop) (congs,thms)
+let val congs' = Library.foldl (gen_rem Drule.eq_thm_prop) (congs,thms)
 in SS{auto_tac=auto_tac, congs= congs',
       cong_net= delete_thms(map mk_trans thms,cong_net),
       mk_simps= normed_rews congs', simps=simps, simp_net=simp_net}
@@ -298,7 +298,7 @@
       simps = simps', simp_net = delete_thms(thms,simp_net)}
 end;
 
-val op delrews = foldl delrew;
+val op delrews = Library.foldl delrew;
 
 
 fun op setauto(SS{congs,cong_net,mk_simps,simps,simp_net,...}, auto_tac) =
@@ -426,9 +426,9 @@
             SOME(thm',_) =>
                     let val ps = prems_of thm and ps' = prems_of thm';
                         val n = length(ps')-length(ps);
-                        val a = length(strip_assums_hyp(nth_elem(i-1,ps)))
+                        val a = length(strip_assums_hyp(List.nth(ps,i-1)))
                         val l = map (fn p => length(strip_assums_hyp(p)))
-                                    (take(n,drop(i-1,ps')));
+                                    (Library.take(n,Library.drop(i-1,ps')));
                     in (simp_refl(rev(l),a,REW::ss),thm',anet,ats,cs) end
           | NONE => (REW::ss,thm,anet,ats,cs);
 
@@ -437,9 +437,9 @@
 fun add_asms(ss,thm,a,anet,ats,cs) =
     let val As = strip_varify(nth_subgoal i thm, a, []);
         val thms = map (trivial o cterm_of(#sign(rep_thm(thm))))As;
-        val new_rws = flat(map mk_rew_rules thms);
-        val rwrls = map mk_trans (flat(map mk_rew_rules thms));
-        val anet' = foldr lhs_insert_thm (rwrls,anet)
+        val new_rws = List.concat(map mk_rew_rules thms);
+        val rwrls = map mk_trans (List.concat(map mk_rew_rules thms));
+        val anet' = Library.foldr lhs_insert_thm (rwrls,anet)
     in  if !tracing andalso not(null new_rws)
         then (writeln"Adding rewrites:";  prths new_rws;  ())
         else ();
@@ -539,7 +539,7 @@
 fun Pinst(f,fT,(eq,eqT),k,i,T,yik,Ts) =
 let fun xn_list(x,n) =
         let val ixs = map (fn i => (x^(radixstring(26,"a",i)),0)) (0 upto n);
-        in ListPair.map eta_Var (ixs, take(n+1,Ts)) end
+        in ListPair.map eta_Var (ixs, Library.take(n+1,Ts)) end
     val lhs = list_comb(f,xn_list("X",k-1))
     val rhs = list_comb(f,xn_list("X",i-1) @ [Bound 0] @ yik)
 in Abs("", T, Const(eq,[fT,fT]--->eqT) $ lhs $ rhs) end;
@@ -596,7 +596,7 @@
     val T' = incr_tvar 9 T;
 in mk_cong_type sg (Const(f,T'),T') end;
 
-fun mk_congs thy = flat o map (mk_cong_thy thy);
+fun mk_congs thy = List.concat o map (mk_cong_thy thy);
 
 fun mk_typed_congs thy =
 let val sg = sign_of thy;
@@ -606,7 +606,7 @@
             val t = case Sign.const_type sg f of
                       SOME(_) => Const(f,T) | NONE => Free(f,T)
         in (t,T) end
-in flat o map (mk_cong_type sg o readfT) end;
+in List.concat o map (mk_cong_type sg o readfT) end;
 
 end (* local *)
 end (* SIMP *);