# HG changeset patch
# User haftmann
# Date 1161356846 -7200
# Node ID 101aefd61aac55a1abe6a94daf76a1ac65401671
# Parent  d6c141871b29a7956bffc03dc640bf01fdc58bd8
slight cleanup

diff -r d6c141871b29 -r 101aefd61aac src/FOLP/simp.ML
--- a/src/FOLP/simp.ML	Fri Oct 20 17:07:25 2006 +0200
+++ b/src/FOLP/simp.ML	Fri Oct 20 17:07:26 2006 +0200
@@ -64,7 +64,7 @@
 
 (*** Indexing and filtering of theorems ***)
 
-fun eq_brl ((b1,th1),(b2,th2)) = b1=b2 andalso Drule.eq_thm_prop (th1,th2);
+fun eq_brl ((b1 : bool, th1), (b2, th2)) = b1 = b2 andalso Drule.eq_thm_prop (th1, th2);
 
 (*insert a thm in a discrimination net by its lhs*)
 fun lhs_insert_thm (th,net) =
@@ -155,25 +155,25 @@
 
 (*ccs contains the names of the constants possessing congruence rules*)
 fun add_hidden_vars ccs =
-  let fun add_hvars(tm,hvars) = case tm of
+  let fun add_hvars tm hvars = case tm of
               Abs(_,_,body) => add_term_vars(body,hvars)
             | _$_ => let val (f,args) = strip_comb tm 
                      in case f of
                             Const(c,T) => 
-                                if c mem ccs
-                                then foldr add_hvars hvars args
-                                else add_term_vars(tm,hvars)
-                          | _ => add_term_vars(tm,hvars)
+                                if member (op =) ccs c
+                                then fold_rev add_hvars args hvars
+                                else add_term_vars (tm, hvars)
+                          | _ => add_term_vars (tm, hvars)
                      end
             | _ => hvars;
   in add_hvars end;
 
 fun add_new_asm_vars new_asms =
-    let fun itf((tm,at),vars) =
+    let fun itf (tm, at) vars =
                 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 vars (tml~~al)
+                   then fold_rev 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 = fold_rev (add_hidden_vars ccs) (lhs::rhs::asms) []
     val hvars = add_new_asm_vars new_asms (rhs,hvars)
-    fun it_asms (asm,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 hvars asms
+    val hvars = fold_rev it_asms asms hvars
     val hvs = map (#1 o dest_Var) hvars
     val refl1_tac = refl_tac 1
     fun norm_step_tac st = st |>
@@ -247,18 +247,18 @@
 (** Insertion of congruences and rewrites **)
 
 (*insert a thm in a thm net*)
-fun insert_thm_warn (th,net) = 
+fun insert_thm_warn th net = 
   Net.insert_term Drule.eq_thm_prop (concl_of th, th) net
   handle Net.INSERT => 
     (writeln"\nDuplicate rewrite or congruence rule:"; print_thm th;
      net);
 
-val insert_thms = foldr insert_thm_warn;
+val insert_thms = fold_rev insert_thm_warn;
 
 fun addrew(SS{auto_tac,congs,cong_net,mk_simps,simps,simp_net}, thm) =
 let val thms = mk_simps thm
 in SS{auto_tac=auto_tac,congs=congs, cong_net=cong_net, mk_simps=mk_simps,
-      simps = (thm,thms)::simps, simp_net = insert_thms simp_net thms}
+      simps = (thm,thms)::simps, simp_net = insert_thms thms simp_net}
 end;
 
 val op addrews = Library.foldl addrew;
@@ -266,25 +266,25 @@
 fun op addcongs(SS{auto_tac,congs,cong_net,mk_simps,simps,simp_net}, thms) =
 let val congs' = thms @ congs;
 in SS{auto_tac=auto_tac, congs= congs',
-      cong_net= insert_thms cong_net (map mk_trans thms),
+      cong_net= insert_thms (map mk_trans thms) cong_net,
       mk_simps= normed_rews congs', simps=simps, simp_net=simp_net}
 end;
 
 (** Deletion of congruences and rewrites **)
 
 (*delete a thm from a thm net*)
-fun delete_thm_warn (th,net) = 
+fun delete_thm_warn th net = 
   Net.delete_term Drule.eq_thm_prop (concl_of th, th) net
   handle Net.DELETE => 
     (writeln"\nNo such rewrite or congruence rule:";  print_thm th;
      net);
 
-val delete_thms = foldr delete_thm_warn;
+val delete_thms = fold_rev delete_thm_warn;
 
 fun op delcongs(SS{auto_tac,congs,cong_net,mk_simps,simps,simp_net}, thms) =
 let val congs' = fold (remove Drule.eq_thm_prop) thms congs
 in SS{auto_tac=auto_tac, congs= congs',
-      cong_net= delete_thms cong_net (map mk_trans thms),
+      cong_net= delete_thms (map mk_trans thms) cong_net,
       mk_simps= normed_rews congs', simps=simps, simp_net=simp_net}
 end;
 
@@ -296,7 +296,7 @@
                            ([],simps'))
     val (thms,simps') = find(simps,[])
 in SS{auto_tac=auto_tac, congs=congs, cong_net=cong_net, mk_simps=mk_simps,
-      simps = simps', simp_net = delete_thms simp_net thms}
+      simps = simps', simp_net = delete_thms thms simp_net }
 end;
 
 val op delrews = Library.foldl delrew;
diff -r d6c141871b29 -r 101aefd61aac src/HOL/Import/replay.ML
--- a/src/HOL/Import/replay.ML	Fri Oct 20 17:07:25 2006 +0200
+++ b/src/HOL/Import/replay.ML	Fri Oct 20 17:07:26 2006 +0200
@@ -27,12 +27,12 @@
 	    end
 	  | rp (PSubst(prfs,ctxt,prf)) thy =
 	    let
-		val (thy',ths) = foldr (fn (p,(thy,ths)) =>
+		val (thy',ths) = fold_rev (fn p => fn (thy, ths) =>
 					   let
 					       val (thy',th) = rp' p thy
 					   in
 					       (thy',th::ths)
-					   end) (thy,[]) prfs
+					   end) prfs (thy,[])
 		val (thy'',th) = rp' prf thy'
 	    in
 		P.SUBST ths ctxt th thy''
diff -r d6c141871b29 -r 101aefd61aac src/HOL/Import/shuffler.ML
--- a/src/HOL/Import/shuffler.ML	Fri Oct 20 17:07:25 2006 +0200
+++ b/src/HOL/Import/shuffler.ML	Fri Oct 20 17:07:26 2006 +0200
@@ -83,7 +83,7 @@
 val copy = I
 val extend = I
 fun merge _ = Library.gen_union Thm.eq_thm
-fun print sg thms =
+fun print _ thms =
     Pretty.writeln (Pretty.big_list "Shuffle theorems:"
 				    (map Display.pretty_thm thms))
 end
@@ -92,7 +92,7 @@
 
 val weaken =
     let
-	val cert = cterm_of (sign_of ProtoPure.thy)
+	val cert = cterm_of ProtoPure.thy
 	val P = Free("P",propT)
 	val Q = Free("Q",propT)
 	val PQ = Logic.mk_implies(P,Q)
@@ -111,7 +111,7 @@
 
 val imp_comm =
     let
-	val cert = cterm_of (sign_of ProtoPure.thy)
+	val cert = cterm_of ProtoPure.thy
 	val P = Free("P",propT)
 	val Q = Free("Q",propT)
 	val R = Free("R",propT)
@@ -131,7 +131,7 @@
 
 val def_norm =
     let
-	val cert = cterm_of (sign_of ProtoPure.thy)
+	val cert = cterm_of ProtoPure.thy
 	val aT = TFree("'a",[])
 	val bT = TFree("'b",[])
 	val v = Free("v",aT)
@@ -158,7 +158,7 @@
 
 val all_comm =
     let
-	val cert = cterm_of (sign_of ProtoPure.thy)
+	val cert = cterm_of ProtoPure.thy
 	val xT = TFree("'a",[])
 	val yT = TFree("'b",[])
 	val P = Free("P",xT-->yT-->propT)
@@ -182,7 +182,7 @@
 
 val equiv_comm =
     let
-	val cert = cterm_of (sign_of ProtoPure.thy)
+	val cert = cterm_of ProtoPure.thy
 	val T    = TFree("'a",[])
 	val t    = Free("t",T)
 	val u    = Free("u",T)
@@ -216,28 +216,28 @@
   | swap_bound n (Abs(x,xT,t)) = Abs(x,xT,swap_bound (n+1) t)
   | swap_bound n t = t
 
-fun rew_th sg (xv as (x,xT)) (yv as (y,yT)) t =
+fun rew_th thy (xv as (x,xT)) (yv as (y,yT)) t =
     let
 	val lhs = list_all ([xv,yv],t)
 	val rhs = list_all ([yv,xv],swap_bound 0 t)
 	val rew = Logic.mk_equals (lhs,rhs)
-	val init = trivial (cterm_of sg rew)
+	val init = trivial (cterm_of thy rew)
     in
 	(all_comm RS init handle e => (message "rew_th"; OldGoals.print_exn e))
     end
 
-fun quant_rewrite sg assumes (t as Const("all",T1) $ (Abs(x,xT,Const("all",T2) $ Abs(y,yT,body)))) =
+fun quant_rewrite thy assumes (t as Const("all",T1) $ (Abs(x,xT,Const("all",T2) $ Abs(y,yT,body)))) =
     let
 	val res = (find_bound 0 body;2) handle RESULT i => i
     in
 	case res of
-	    0 => SOME (rew_th sg (x,xT) (y,yT) body)
+	    0 => SOME (rew_th thy (x,xT) (y,yT) body)
 	  | 1 => if string_ord(y,x) = LESS
 		 then
 		     let
 			 val newt = Const("all",T1) $ (Abs(y,xT,Const("all",T2) $ Abs(x,yT,body)))
-			 val t_th    = reflexive (cterm_of sg t)
-			 val newt_th = reflexive (cterm_of sg newt)
+			 val t_th    = reflexive (cterm_of thy t)
+			 val newt_th = reflexive (cterm_of thy newt)
 		     in
 			 SOME (transitive t_th newt_th)
 		     end
@@ -264,10 +264,10 @@
 		  | _ => error "Internal error in Shuffler.freeze_thaw") type_inst)
     end
 
-fun inst_tfrees sg [] thm = thm
-  | inst_tfrees sg ((name,U)::rest) thm = 
+fun inst_tfrees thy [] thm = thm
+  | inst_tfrees thy ((name,U)::rest) thm = 
     let
-	val cU = ctyp_of sg U
+	val cU = ctyp_of thy U
 	val tfrees = add_term_tfrees (prop_of thm,[])
 	val (rens, thm') = Thm.varifyT'
     (remove (op = o apsnd fst) name tfrees) thm
@@ -275,10 +275,10 @@
 	    case rens of
 		[] => thm'
 	      | [((_, S), idx)] => instantiate
-            ([(ctyp_of sg (TVar (idx, S)), cU)], []) thm'
+            ([(ctyp_of thy (TVar (idx, S)), cU)], []) thm'
 	      | _ => error "Shuffler.inst_tfrees internal error"
     in
-	inst_tfrees sg rest mid
+	inst_tfrees thy rest mid
     end
 
 fun is_Abs (Abs _) = true
@@ -295,11 +295,11 @@
     end
   | eta_redex _ = false
 
-fun eta_contract sg assumes origt =
+fun eta_contract thy assumes origt =
     let
 	val (typet,Tinst) = freeze_thaw_term origt
-	val (init,thaw) = freeze_thaw (reflexive (cterm_of sg typet))
-	val final = inst_tfrees sg Tinst o thaw
+	val (init,thaw) = freeze_thaw (reflexive (cterm_of thy typet))
+	val final = inst_tfrees thy Tinst o thaw
 	val t = #1 (Logic.dest_equals (prop_of init))
 	val _ =
 	    let
@@ -307,11 +307,11 @@
 	    in
 		if not (lhs aconv origt)
 		then (writeln "Something is utterly wrong: (orig,lhs,frozen type,t,tinst)";
-		      writeln (string_of_cterm (cterm_of sg origt));
-		      writeln (string_of_cterm (cterm_of sg lhs));
-		      writeln (string_of_cterm (cterm_of sg typet));
-		      writeln (string_of_cterm (cterm_of sg t));
-		      app (fn (n,T) => writeln (n ^ ": " ^ (string_of_ctyp (ctyp_of sg T)))) Tinst;
+		      writeln (string_of_cterm (cterm_of thy origt));
+		      writeln (string_of_cterm (cterm_of thy lhs));
+		      writeln (string_of_cterm (cterm_of thy typet));
+		      writeln (string_of_cterm (cterm_of thy t));
+		      app (fn (n,T) => writeln (n ^ ": " ^ (string_of_ctyp (ctyp_of thy T)))) Tinst;
 		      writeln "done")
 		else ()
 	    end
@@ -321,7 +321,7 @@
 	    ((if eta_redex P andalso eta_redex Q
 	      then
 		  let
-		      val cert = cterm_of sg
+		      val cert = cterm_of thy
 		      val v = Free(Name.variant (add_term_free_names(t,[])) "v",xT)
 		      val cv = cert v
 		      val ct = cert t
@@ -347,21 +347,21 @@
 	  | _ => NONE
        end
 
-fun beta_fun sg assume t =
-    SOME (beta_conversion true (cterm_of sg t))
+fun beta_fun thy assume t =
+    SOME (beta_conversion true (cterm_of thy t))
 
 val meta_sym_rew = thm "refl"
 
-fun equals_fun sg assume t =
+fun equals_fun thy assume t =
     case t of
 	Const("op ==",_) $ u $ v => if Term.term_ord (u,v) = LESS then SOME (meta_sym_rew) else NONE
       | _ => NONE
 
-fun eta_expand sg assumes origt =
+fun eta_expand thy assumes origt =
     let
 	val (typet,Tinst) = freeze_thaw_term origt
-	val (init,thaw) = freeze_thaw (reflexive (cterm_of sg typet))
-	val final = inst_tfrees sg Tinst o thaw
+	val (init,thaw) = freeze_thaw (reflexive (cterm_of thy typet))
+	val final = inst_tfrees thy Tinst o thaw
 	val t = #1 (Logic.dest_equals (prop_of init))
 	val _ =
 	    let
@@ -369,11 +369,11 @@
 	    in
 		if not (lhs aconv origt)
 		then (writeln "Something is utterly wrong: (orig,lhs,frozen type,t,tinst)";
-		      writeln (string_of_cterm (cterm_of sg origt));
-		      writeln (string_of_cterm (cterm_of sg lhs));
-		      writeln (string_of_cterm (cterm_of sg typet));
-		      writeln (string_of_cterm (cterm_of sg t));
-		      app (fn (n,T) => writeln (n ^ ": " ^ (string_of_ctyp (ctyp_of sg T)))) Tinst;
+		      writeln (string_of_cterm (cterm_of thy origt));
+		      writeln (string_of_cterm (cterm_of thy lhs));
+		      writeln (string_of_cterm (cterm_of thy typet));
+		      writeln (string_of_cterm (cterm_of thy t));
+		      app (fn (n,T) => writeln (n ^ ": " ^ (string_of_ctyp (ctyp_of thy T)))) Tinst;
 		      writeln "done")
 		else ()
 	    end
@@ -384,7 +384,7 @@
 	    then (case domain_type T of
 		      Type("fun",[aT,bT]) =>
 		      let
-			  val cert = cterm_of sg
+			  val cert = cterm_of thy
 			  val vname = Name.variant (add_term_free_names(t,[])) "v"
 			  val v = Free(vname,aT)
 			  val cv = cert v
@@ -409,7 +409,7 @@
 		      end
 		    | _ => NONE)
 	    else NONE
-	  | _ => (error ("Bad eta_expand argument" ^ (string_of_cterm (cterm_of sg t))); NONE)
+	  | _ => (error ("Bad eta_expand argument" ^ (string_of_cterm (cterm_of thy t))); NONE)
     end
     handle e => (writeln "eta_expand internal error"; OldGoals.print_exn e)
 
@@ -423,30 +423,30 @@
 val S  = mk_free "S" xT
 val S'  = mk_free "S'" xT
 in
-fun beta_simproc sg = Simplifier.simproc_i
-		      sg
+fun beta_simproc thy = Simplifier.simproc_i
+		      thy
 		      "Beta-contraction"
 		      [Abs("x",xT,Q) $ S]
 		      beta_fun
 
-fun equals_simproc sg = Simplifier.simproc_i
-		      sg
+fun equals_simproc thy = Simplifier.simproc_i
+		      thy
 		      "Ordered rewriting of meta equalities"
 		      [Const("op ==",xT) $ S $ S']
 		      equals_fun
 
-fun quant_simproc sg = Simplifier.simproc_i
-			   sg
+fun quant_simproc thy = Simplifier.simproc_i
+			   thy
 			   "Ordered rewriting of nested quantifiers"
 			   [all xT $ (Abs("x",xT,all yT $ (Abs("y",yT,P $ Bound 1 $ Bound 0))))]
 			   quant_rewrite
-fun eta_expand_simproc sg = Simplifier.simproc_i
-			 sg
+fun eta_expand_simproc thy = Simplifier.simproc_i
+			 thy
 			 "Smart eta-expansion by equivalences"
 			 [Logic.mk_equals(Q,R)]
 			 eta_expand
-fun eta_contract_simproc sg = Simplifier.simproc_i
-			 sg
+fun eta_contract_simproc thy = Simplifier.simproc_i
+			 thy
 			 "Smart handling of eta-contractions"
 			 [all xT $ (Abs("x",xT,Logic.mk_equals(Q $ Bound 0,R $ Bound 0)))]
 			 eta_contract
@@ -455,7 +455,7 @@
 (* Disambiguates the names of bound variables in a term, returning t
 == t' where all the names of bound variables in t' are unique *)
 
-fun disamb_bound sg t =
+fun disamb_bound thy t =
     let
 	
 	fun F (t $ u,idx) =
@@ -474,8 +474,8 @@
 	    end
 	  | F arg = arg
 	val (t',_) = F (t,0)
-	val ct = cterm_of sg t
-	val ct' = cterm_of sg t'
+	val ct = cterm_of thy t
+	val ct' = cterm_of thy t'
 	val res = transitive (reflexive ct) (reflexive ct')
 	val _ = message ("disamb_term: " ^ (string_of_thm res))
     in
@@ -488,12 +488,11 @@
 
 fun norm_term thy t =
     let
-	val sg = sign_of thy
 	val norms = ShuffleData.get thy
 	val ss = Simplifier.theory_context thy empty_ss
           setmksimps single
-	  addsimps (map (Thm.transfer sg) norms)
-          addsimprocs [quant_simproc sg, eta_expand_simproc sg,eta_contract_simproc sg]
+	  addsimps (map (Thm.transfer thy) norms)
+          addsimprocs [quant_simproc thy, eta_expand_simproc thy,eta_contract_simproc thy]
 	fun chain f th =
 	    let
                 val rhs = snd (dest_equals (cprop_of th))
@@ -501,7 +500,7 @@
 		transitive th (f rhs)
 	    end
 	val th =
-            t |> disamb_bound sg
+            t |> disamb_bound thy
 	      |> chain (Simplifier.full_rewrite ss)
               |> chain eta_conversion
 	      |> strip_shyps
@@ -509,7 +508,7 @@
     in
 	th
     end
-    handle e => (writeln "norm_term internal error"; print_sign_exn (sign_of thy) e)
+    handle e => (writeln "norm_term internal error"; print_sign_exn thy e)
 
 
 (* Closes a theorem with respect to free and schematic variables (does
@@ -517,11 +516,11 @@
 
 fun close_thm th =
     let
-	val sg = sign_of_thm th
+	val thy = sign_of_thm th
 	val c = prop_of th
 	val vars = add_term_frees (c,add_term_vars(c,[]))
     in
-	Drule.forall_intr_list (map (cterm_of sg) vars) th
+	Drule.forall_intr_list (map (cterm_of thy) vars) th
     end
     handle e => (writeln "close_thm internal error"; OldGoals.print_exn e)
 
@@ -534,14 +533,14 @@
 	equal_elim (norm_term thy c) th
     end
 
-(* make_equal sg t u tries to construct the theorem t == u under the
-signature sg.  If it succeeds, SOME (t == u) is returned, otherwise
+(* make_equal thy t u tries to construct the theorem t == u under the
+signature thy.  If it succeeds, SOME (t == u) is returned, otherwise
 NONE is returned. *)
 
-fun make_equal sg t u =
+fun make_equal thy t u =
     let
-	val t_is_t' = norm_term sg t
-	val u_is_u' = norm_term sg u
+	val t_is_t' = norm_term thy t
+	val u_is_u' = norm_term thy u
 	val th = transitive t_is_t' (symmetric u_is_u')
 	val _ = message ("make_equal: SOME " ^ (string_of_thm th))
     in
@@ -569,7 +568,7 @@
     end
     
 val collect_ignored =
-    foldr (fn (thm,cs) =>
+    fold_rev (fn thm => fn cs =>
 	      let
 		  val (lhs,rhs) = Logic.dest_equals (prop_of thm)
 		  val ignore_lhs = term_consts lhs \\ term_consts rhs
@@ -584,10 +583,9 @@
 
 fun set_prop thy t =
     let
-	val sg = sign_of thy
 	val vars = add_term_frees (t,add_term_vars (t,[]))
-	val closed_t = foldr (fn (v,body) => let val vT = type_of v
-					     in all vT $ (Abs("x",vT,abstract_over(v,body))) end) t vars
+	val closed_t = Library.foldr (fn (v, body) =>
+      let val vT = type_of v in all vT $ (Abs ("x", vT, abstract_over (v, body))) end) (vars, t)
 	val rew_th = norm_term thy closed_t
 	val rhs = snd (dest_equals (cprop_of rew_th))
 
@@ -595,7 +593,7 @@
 	fun process [] = NONE
 	  | process ((name,th)::thms) =
 	    let
-		val norm_th = Thm.varifyT (norm_thm thy (close_thm (Thm.transfer sg th)))
+		val norm_th = Thm.varifyT (norm_thm thy (close_thm (Thm.transfer thy th)))
 		val triv_th = trivial rhs
 		val _ = message ("Shuffler.set_prop: Gluing together " ^ (string_of_thm norm_th) ^ " and " ^ (string_of_thm triv_th))
 		val mod_th = case Seq.pull (bicompose false (*true*) (false,norm_th,0) 1 triv_th) of
@@ -608,7 +606,7 @@
 			val closed_th = equal_elim (symmetric rew_th) mod_th
 		    in
 			message ("Shuffler.set_prop succeeded by " ^ name);
-			SOME (name,forall_elim_list (map (cterm_of sg) vars) closed_th)
+			SOME (name,forall_elim_list (map (cterm_of thy) vars) closed_th)
 		    end
 		  | NONE => process thms
 	    end
@@ -626,7 +624,7 @@
 fun find_potential thy t =
     let
 	val shuffles = ShuffleData.get thy
-	val ignored = collect_ignored [] shuffles
+	val ignored = collect_ignored shuffles []
 	val rel_consts = term_consts t \\ ignored
 	val pot_thms = PureThy.thms_containing_consts thy rel_consts
     in
diff -r d6c141871b29 -r 101aefd61aac src/HOL/Integ/cooper_dec.ML
--- a/src/HOL/Integ/cooper_dec.ML	Fri Oct 20 17:07:25 2006 +0200
+++ b/src/HOL/Integ/cooper_dec.ML	Fri Oct 20 17:07:26 2006 +0200
@@ -443,7 +443,7 @@
    val ts = coeffs_of t
    in case ts of
      [] => raise DVD_UNKNOWN
-    |_  => foldr (fn(k,r) => r andalso (k mod dn = 0)) true ts
+    |_  => fold_rev (fn k => fn r => r andalso (k mod dn = 0)) ts true
    end;
 
 
@@ -736,7 +736,7 @@
              in (rw,HOLogic.mk_disj(F',rf)) 
 	     end)
     val f = if b then linear_add else linear_sub
-    val p_elements = foldr (fn (i,l) => l union (map (fn e => f [] e (mk_numeral i)) st)) [] (myupto 1 d)
+    val p_elements = fold_rev (fn i => fn l => l union (map (fn e => f [] e (mk_numeral i)) st)) (myupto 1 d) []
     in h p_elements
     end;
 
diff -r d6c141871b29 -r 101aefd61aac src/HOL/Nominal/nominal_permeq.ML
--- a/src/HOL/Nominal/nominal_permeq.ML	Fri Oct 20 17:07:25 2006 +0200
+++ b/src/HOL/Nominal/nominal_permeq.ML	Fri Oct 20 17:07:26 2006 +0200
@@ -268,9 +268,9 @@
             val ps = Logic.strip_params (term_of goal);
             val Ts = rev (map snd ps);
             val vs = collect_vars 0 x [];
-            val s = foldr (fn (v, s) =>
+            val s = Library.foldr (fn (v, s) =>
                 HOLogic.pair_const (fastype_of1 (Ts, v)) (fastype_of1 (Ts, s)) $ v $ s)
-              HOLogic.unit vs;
+              (vs, HOLogic.unit);
             val s' = list_abs (ps,
               Const ("Nominal.supp", fastype_of1 (Ts, s) --> body_type T) $ s);
             val supports_rule' = Thm.lift_rule goal supports_rule;
@@ -305,9 +305,9 @@
             val ps = Logic.strip_params (term_of goal);
             val Ts = rev (map snd ps);
             val vs = collect_vars 0 t [];
-            val s = foldr (fn (v, s) =>
+            val s = Library.foldr (fn (v, s) =>
                 HOLogic.pair_const (fastype_of1 (Ts, v)) (fastype_of1 (Ts, s)) $ v $ s)
-              HOLogic.unit vs;
+              (vs, HOLogic.unit);
             val s' = list_abs (ps,
               Const ("Nominal.supp", fastype_of1 (Ts, s) --> (HOLogic.mk_setT T)) $ s);
             val supports_fresh_rule' = Thm.lift_rule goal supports_fresh_rule;
diff -r d6c141871b29 -r 101aefd61aac src/HOL/Real/ferrante_rackoff.ML
--- a/src/HOL/Real/ferrante_rackoff.ML	Fri Oct 20 17:07:25 2006 +0200
+++ b/src/HOL/Real/ferrante_rackoff.ML	Fri Oct 20 17:07:26 2006 +0200
@@ -5,94 +5,85 @@
 Ferrante and Rackoff Algorithm.
 *)
 
-structure Ferrante_Rackoff:
+signature FERRANTE_RACKOFF =
 sig
-  val trace : bool ref
-  val ferrack_tac : bool -> int -> tactic
-  val setup : theory -> theory
-end =
+  val ferrack_tac: bool -> int -> tactic
+  val setup: theory -> theory
+  val trace: bool ref
+end;
+
+structure Ferrante_Rackoff : FERRANTE_RACKOFF =
 struct
 
 val trace = ref false;
 fun trace_msg s = if !trace then tracing s else ();
 
-val context_ss = simpset_of (the_context ());
-
-val nT = HOLogic.natT;
-val binarith = map thm
-  ["Pls_0_eq", "Min_1_eq",
- "pred_Pls","pred_Min","pred_1","pred_0",
+val binarith = map thm ["Pls_0_eq", "Min_1_eq", "pred_Pls", "pred_Min","pred_1","pred_0",
   "succ_Pls", "succ_Min", "succ_1", "succ_0",
-  "add_Pls", "add_Min", "add_BIT_0", "add_BIT_10",
-  "add_BIT_11", "minus_Pls", "minus_Min", "minus_1", 
-  "minus_0", "mult_Pls", "mult_Min", "mult_1", "mult_0", 
+  "add_Pls", "add_Min", "add_BIT_0", "add_BIT_10", "add_BIT_11",
+  "minus_Pls", "minus_Min", "minus_1", "minus_0",
+  "mult_Pls", "mult_Min", "mult_1", "mult_0", 
   "add_Pls_right", "add_Min_right"];
- val intarithrel = 
-     (map thm ["int_eq_number_of_eq","int_neg_number_of_BIT", 
-		"int_le_number_of_eq","int_iszero_number_of_0",
-		"int_less_number_of_eq_neg"]) @
-     (map (fn s => thm s RS thm "lift_bool") 
-	  ["int_iszero_number_of_Pls","int_iszero_number_of_1",
-	   "int_neg_number_of_Min"])@
-     (map (fn s => thm s RS thm "nlift_bool") 
-	  ["int_nonzero_number_of_Min","int_not_neg_number_of_Pls"]);
-     
+
+val intarithrel = 
+  map thm ["int_eq_number_of_eq", "int_neg_number_of_BIT", "int_le_number_of_eq",
+    "int_iszero_number_of_0", "int_less_number_of_eq_neg"]
+  @ map (fn s => thm s RS thm "lift_bool") ["int_iszero_number_of_Pls",
+    "int_iszero_number_of_1", "int_neg_number_of_Min"]
+  @ map (fn s => thm s RS thm "nlift_bool") ["int_nonzero_number_of_Min",
+    "int_not_neg_number_of_Pls"];
+ 
 val intarith = map thm ["int_number_of_add_sym", "int_number_of_minus_sym",
-			"int_number_of_diff_sym", "int_number_of_mult_sym"];
+  "int_number_of_diff_sym", "int_number_of_mult_sym"];
+
 val natarith = map thm ["add_nat_number_of", "diff_nat_number_of",
-			"mult_nat_number_of", "eq_nat_number_of",
-			"less_nat_number_of"]
-val powerarith = 
-    (map thm ["nat_number_of", "zpower_number_of_even", 
-	      "zpower_Pls", "zpower_Min"]) @ 
-    [(Tactic.simplify true [thm "zero_eq_Numeral0_nring", 
-			   thm "one_eq_Numeral1_nring"] 
-  (thm "zpower_number_of_odd"))]
+  "mult_nat_number_of", "eq_nat_number_of", "less_nat_number_of"];
+
+val powerarith =
+  map thm ["nat_number_of", "zpower_number_of_even",
+  "zpower_Pls", "zpower_Min"]
+  @ [Tactic.simplify true [thm "zero_eq_Numeral0_nring", thm "one_eq_Numeral1_nring"]
+    (thm "zpower_number_of_odd")]
 
 val comp_arith = binarith @ intarith @ intarithrel @ natarith 
-	    @ powerarith @[thm"not_false_eq_true", thm "not_true_eq_false"];
+  @ powerarith @ [thm "not_false_eq_true", thm "not_true_eq_false"];
 
-fun prepare_for_linr sg q fm = 
+fun prepare_for_linr q fm = 
   let
     val ps = Logic.strip_params fm
     val hs = map HOLogic.dest_Trueprop (Logic.strip_assums_hyp fm)
     val c = HOLogic.dest_Trueprop (Logic.strip_assums_concl fm)
-    fun mk_all ((s, T), (P,n)) =
+    fun mk_all ((s, T), (P, n)) =
       if 0 mem loose_bnos P then
         (HOLogic.all_const T $ Abs (s, T, P), n)
       else (incr_boundvars ~1 P, n-1)
     fun mk_all2 (v, t) = HOLogic.all_const (fastype_of v) $ lambda v t;
-      val rhs = hs
-(*    val (rhs,irhs) = List.partition (relevant (rev ps)) hs *)
-    val np = length ps
-    val (fm',np) =  foldr (fn ((x, T), (fm,n)) => mk_all ((x, T), (fm,n)))
-      (foldr HOLogic.mk_imp c rhs, np) ps
-    val (vs, _) = List.partition (fn t => q orelse (type_of t) = nT)
+    val rhs = hs;
+    val np = length ps;
+    val (fm', np) = Library.foldr mk_all (ps, (Library.foldr HOLogic.mk_imp (rhs, c), np));
+    val (vs, _) = List.partition (fn t => q orelse (type_of t) = HOLogic.natT)
       (term_frees fm' @ term_vars fm');
-    val fm2 = foldr mk_all2 fm' vs
+    val fm2 = Library.foldr mk_all2 (vs, fm');
   in (fm2, np + length vs, length rhs) end;
 
-(*Object quantifier to meta --*)
-fun spec_step n th = if (n=0) then th else (spec_step (n-1) th) RS spec ;
-
-(* object implication to meta---*)
-fun mp_step n th = if (n=0) then th else (mp_step (n-1) th) RS mp;
-
+fun spec_step n th = if n = 0 then th else spec_step (n - 1) th RS spec ;
+fun mp_step n th = if n = 0 then th else mp_step (n - 1) th RS mp;
 
-fun ferrack_tac q i = 
-    (ObjectLogic.atomize_tac i) 
-	THEN (REPEAT_DETERM (split_tac [split_min, split_max,abs_split] i))
-	THEN (fn st =>
+local
+  val context_ss = simpset_of (the_context ())
+in fun ferrack_tac q i =  ObjectLogic.atomize_tac i
+  THEN REPEAT_DETERM (split_tac [split_min, split_max,abs_split] i)
+  THEN (fn st =>
   let
-    val g = List.nth (prems_of st, i - 1)
-    val sg = sign_of_thm st
+    val g = nth (prems_of st) (i - 1)
+    val thy = sign_of_thm st
     (* Transform the term*)
-    val (t,np,nh) = prepare_for_linr sg q g
+    val (t,np,nh) = prepare_for_linr q g
     (* Some simpsets for dealing with mod div abs and nat*)
     val simpset0 = HOL_basic_ss addsimps comp_arith addsplits [split_min, split_max]
     (* simp rules for elimination of abs *)
     val simpset3 = HOL_basic_ss addsplits [abs_split]
-    val ct = cterm_of sg (HOLogic.mk_Trueprop t)
+    val ct = cterm_of thy (HOLogic.mk_Trueprop t)
     (* Theorem for the nat --> int transformation *)
     val pre_thm = Seq.hd (EVERY
       [simp_tac simpset0 1, TRY (simp_tac context_ss 1)]
@@ -101,10 +92,10 @@
     (* The result of the quantifier elimination *)
     val (th, tac) = case (prop_of pre_thm) of
         Const ("==>", _) $ (Const ("Trueprop", _) $ t1) $ _ =>
-    let val pth = Ferrante_Rackoff_Proof.qelim (cterm_of sg (Pattern.eta_long [] t1))
+    let val pth = Ferrante_Rackoff_Proof.qelim (cterm_of thy (Pattern.eta_long [] t1))
     in 
           (trace_msg ("calling procedure with term:\n" ^
-             Sign.string_of_term sg t1);
+             Sign.string_of_term thy t1);
            ((pth RS iffD2) RS pre_thm,
             assm_tac (i + 1) THEN (if q then I else TRY) (rtac TrueI i)))
     end
@@ -112,10 +103,11 @@
   in (rtac (((mp_step nh) o (spec_step np)) th) i 
       THEN tac) st
   end handle Subscript => no_tac st | Ferrante_Rackoff_Proof.FAILURE _ => no_tac st);
+end; (*local*)
 
 fun ferrack_args meth =
- let val parse_flag = 
-         Args.$$$ "no_quantify" >> (K (K false));
+ let
+   val parse_flag =  Args.$$$ "no_quantify" >> (K (K false));
  in
    Method.simple_args 
   (Scan.optional (Args.$$$ "(" |-- Scan.repeat1 parse_flag --| Args.$$$ ")") [] >>
diff -r d6c141871b29 -r 101aefd61aac src/HOL/Tools/Presburger/cooper_dec.ML
--- a/src/HOL/Tools/Presburger/cooper_dec.ML	Fri Oct 20 17:07:25 2006 +0200
+++ b/src/HOL/Tools/Presburger/cooper_dec.ML	Fri Oct 20 17:07:26 2006 +0200
@@ -443,7 +443,7 @@
    val ts = coeffs_of t
    in case ts of
      [] => raise DVD_UNKNOWN
-    |_  => foldr (fn(k,r) => r andalso (k mod dn = 0)) true ts
+    |_  => fold_rev (fn k => fn r => r andalso (k mod dn = 0)) ts true
    end;
 
 
@@ -736,7 +736,7 @@
              in (rw,HOLogic.mk_disj(F',rf)) 
 	     end)
     val f = if b then linear_add else linear_sub
-    val p_elements = foldr (fn (i,l) => l union (map (fn e => f [] e (mk_numeral i)) st)) [] (myupto 1 d)
+    val p_elements = fold_rev (fn i => fn l => l union (map (fn e => f [] e (mk_numeral i)) st)) (myupto 1 d) []
     in h p_elements
     end;
 
diff -r d6c141871b29 -r 101aefd61aac src/HOL/Tools/datatype_prop.ML
--- a/src/HOL/Tools/datatype_prop.ML	Fri Oct 20 17:07:25 2006 +0200
+++ b/src/HOL/Tools/datatype_prop.ML	Fri Oct 20 17:07:26 2006 +0200
@@ -64,24 +64,23 @@
 
 fun make_injs descr sorts =
   let
-    val descr' = List.concat descr;
-
-    fun make_inj T ((cname, cargs), injs) =
-      if null cargs then injs else
+    val descr' = flat descr;
+    fun make_inj T (cname, cargs) =
+      if null cargs then I else
         let
           val Ts = map (typ_of_dtyp descr' sorts) cargs;
           val constr_t = Const (cname, Ts ---> T);
           val tnames = make_tnames Ts;
           val frees = map Free (tnames ~~ Ts);
           val frees' = map Free ((map ((op ^) o (rpair "'")) tnames) ~~ Ts);
-        in (HOLogic.mk_Trueprop (HOLogic.mk_eq
+        in cons (HOLogic.mk_Trueprop (HOLogic.mk_eq
           (HOLogic.mk_eq (list_comb (constr_t, frees), list_comb (constr_t, frees')),
            foldr1 (HOLogic.mk_binop "op &")
-             (map HOLogic.mk_eq (frees ~~ frees')))))::injs
+             (map HOLogic.mk_eq (frees ~~ frees')))))
         end;
-
-  in map (fn (d, T) => foldr (make_inj T) [] (#3 (snd d)))
-    ((hd descr) ~~ Library.take (length (hd descr), get_rec_types descr' sorts))
+  in
+    map2 (fn d => fn T => fold_rev (make_inj T) (#3 (snd d)) [])
+      (hd descr) (Library.take (length (hd descr), get_rec_types descr' sorts))
   end;
 
 (********************************* induction **********************************)
diff -r d6c141871b29 -r 101aefd61aac src/HOL/Tools/recdef_package.ML
--- a/src/HOL/Tools/recdef_package.ML	Fri Oct 20 17:07:25 2006 +0200
+++ b/src/HOL/Tools/recdef_package.ML	Fri Oct 20 17:07:26 2006 +0200
@@ -80,8 +80,6 @@
     val (del, rest) = List.partition (Library.equal c o fst) congs;
   in if null del then (warning ("No recdef congruence rule for " ^ quote c); congs) else rest end;
 
-val add_congs = foldr (uncurry add_cong);
-
 end;
 
 
diff -r d6c141871b29 -r 101aefd61aac src/HOL/Tools/record_package.ML
--- a/src/HOL/Tools/record_package.ML	Fri Oct 20 17:07:25 2006 +0200
+++ b/src/HOL/Tools/record_package.ML	Fri Oct 20 17:07:26 2006 +0200
@@ -491,7 +491,7 @@
 
 
 fun record_update_tr [t, u] =
-      foldr (op $) t (rev (gen_fields_tr "_updates" "_update" updateN u))
+      Library.foldr (op $) (rev (gen_fields_tr "_updates" "_update" updateN u), t)
   | record_update_tr ts = raise TERM ("record_update_tr", ts);
 
 fun update_name_tr (Free (x, T) :: ts) = Free (suffix updateN x, T) $$ ts
@@ -1547,8 +1547,8 @@
 (* mk_recordT builds up the record type from the current extension tpye extT and a list
  * of parent extensions, starting with the root of the record hierarchy
 *)
-fun mk_recordT extT parent_exts =
-    foldr (fn ((parent,Ts),T) => Type (parent, subst_last T Ts)) extT parent_exts;
+fun mk_recordT extT =
+    fold_rev (fn (parent, Ts) => fn T => Type (parent, subst_last T Ts)) extT;
 
 
 
@@ -1646,12 +1646,12 @@
     val extension_id = Library.foldl (op ^) ("",extension_names);
 
 
-    fun rec_schemeT n = mk_recordT extT (map #extension (prune n parents));
+    fun rec_schemeT n = mk_recordT (map #extension (prune n parents)) extT;
     val rec_schemeT0 = rec_schemeT 0;
 
     fun recT n =
       let val (c,Ts) = extension
-      in mk_recordT (Type (c,subst_last HOLogic.unitT Ts))(map #extension (prune n parents))
+      in mk_recordT (map #extension (prune n parents)) (Type (c,subst_last HOLogic.unitT Ts))
       end;
     val recT0 = recT 0;
 
diff -r d6c141871b29 -r 101aefd61aac src/HOL/Tools/refute.ML
--- a/src/HOL/Tools/refute.ML	Fri Oct 20 17:07:25 2006 +0200
+++ b/src/HOL/Tools/refute.ML	Fri Oct 20 17:07:26 2006 +0200
@@ -421,8 +421,8 @@
 		(* (string * Term.term) list *)
 		val axioms = Theory.all_axioms_of thy;
 		(* string list *)
-		val rec_names = Symtab.fold (fn (_, info) => fn acc =>
-			#rec_names info @ acc) (DatatypePackage.get_datatypes thy) []
+		val rec_names = Symtab.fold (append o #rec_names o snd)
+          (DatatypePackage.get_datatypes thy) [];
 		(* string list *)
 		val const_of_class_names = map Logic.const_of_class (Sign.classes thy)
 		(* given a constant 's' of type 'T', which is a subterm of 't', where  *)
@@ -677,7 +677,7 @@
 					fun is_IDT_recursor () =
 						(* I'm not quite sure if checking the name 's' is sufficient, *)
 						(* or if we should also check the type 'T'                    *)
-						s mem rec_names
+						member (op =) rec_names s
 				in
 					if is_const_of_class () then
 						(* axiomatic type classes: add "OFCLASS(?'a::c, c_class)" and *)
diff -r d6c141871b29 -r 101aefd61aac src/HOL/ex/reflection.ML
--- a/src/HOL/ex/reflection.ML	Fri Oct 20 17:07:25 2006 +0200
+++ b/src/HOL/ex/reflection.ML	Fri Oct 20 17:07:26 2006 +0200
@@ -184,8 +184,8 @@
        val tml = Vartab.dest tmenv
        val SOME (_,t') = AList.lookup (op =) tml (xn,0)
        val cvs = 
-	   cert (foldr (fn (x,xs) => Const("List.list.Cons", ntT --> ntlT --> ntlT)$x$xs) 
-		       (Free(vsn,ntlT)) bsT)
+	   cert (fold_rev (fn x => fn xs => Const("List.list.Cons", ntT --> ntlT --> ntlT)$x$xs)
+		       bsT (Free (vsn, ntlT)))
        val cts = map (fn ((vn,vi),(tT,t)) => (cert(Var ((vn,vi),tT)), cert t)) 
 		     (AList.delete (op =) (xn,0) tml)
        val th = (instantiate 
@@ -232,12 +232,12 @@
 
 fun mk_congs ctxt raw_eqs = 
  let 
-  val fs = foldr (fn (eq,fns) => 
+  val fs = fold_rev (fn eq =>
 		     insert (op =) (eq |> prop_of |> HOLogic.dest_Trueprop 
 			 |> HOLogic.dest_eq |> fst |> strip_comb 
-			 |> fst) fns) [] raw_eqs
-  val tys = foldr (fn (f,ts) => (f |> fastype_of |> binder_types |> split_last |> fst) 
-				    union ts) [] fs
+			 |> fst)) raw_eqs []
+  val tys = fold_rev (fn f => fn ts => (f |> fastype_of |> binder_types |> split_last |> fst) 
+				    union ts) fs []
   val _ = bds := AList.make (fn _ => ([],[])) tys
   val (vs, ctxt') = Variable.variant_fixes (replicate (length tys) "vs") ctxt
   val thy = ProofContext.theory_of ctxt'
diff -r d6c141871b29 -r 101aefd61aac src/HOL/ex/svc_funcs.ML
--- a/src/HOL/ex/svc_funcs.ML	Fri Oct 20 17:07:25 2006 +0200
+++ b/src/HOL/ex/svc_funcs.ML	Fri Oct 20 17:07:26 2006 +0200
@@ -119,7 +119,7 @@
    in #1 o tag end;
 
  (*Map expression e to 0<=a --> e, where "a" is the name of a nat variable*)
- fun add_nat_var (a, e) =
+ fun add_nat_var a e =
      Buildin("=>", [Buildin("<=", [Int 0, UnInterp (a, [])]),
                     e]);
 
@@ -240,7 +240,7 @@
 
       val body_e = mt pos body  (*evaluate now to assign into !nat_vars*)
   in
-     foldr add_nat_var body_e (!nat_vars)
+     fold_rev add_nat_var (!nat_vars) body_e
   end;
 
 
diff -r d6c141871b29 -r 101aefd61aac src/HOL/hologic.ML
--- a/src/HOL/hologic.ML	Fri Oct 20 17:07:25 2006 +0200
+++ b/src/HOL/hologic.ML	Fri Oct 20 17:07:26 2006 +0200
@@ -165,7 +165,7 @@
 
 fun all_const T = Const ("All", [T --> boolT] ---> boolT);
 fun mk_all (x, T, P) = all_const T $ absfree (x, T, P);
-fun list_all (vs,x) = foldr (fn ((x, T), P) => all_const T $ Abs (x, T, P)) x vs;
+fun list_all (vs,x) = Library.foldr (fn ((x, T), P) => all_const T $ Abs (x, T, P)) (vs, x);
 
 fun exists_const T = Const ("Ex", [T --> boolT] ---> boolT);
 fun mk_exists (x, T, P) = exists_const T $ absfree (x, T, P);