slight cleanup
authorhaftmann
Fri Oct 20 17:07:26 2006 +0200 (2006-10-20)
changeset 21078101aefd61aac
parent 21077 d6c141871b29
child 21079 747d716e98d0
slight cleanup
src/FOLP/simp.ML
src/HOL/Import/replay.ML
src/HOL/Import/shuffler.ML
src/HOL/Integ/cooper_dec.ML
src/HOL/Nominal/nominal_permeq.ML
src/HOL/Real/ferrante_rackoff.ML
src/HOL/Tools/Presburger/cooper_dec.ML
src/HOL/Tools/datatype_prop.ML
src/HOL/Tools/recdef_package.ML
src/HOL/Tools/record_package.ML
src/HOL/Tools/refute.ML
src/HOL/ex/reflection.ML
src/HOL/ex/svc_funcs.ML
src/HOL/hologic.ML
     1.1 --- a/src/FOLP/simp.ML	Fri Oct 20 17:07:25 2006 +0200
     1.2 +++ b/src/FOLP/simp.ML	Fri Oct 20 17:07:26 2006 +0200
     1.3 @@ -64,7 +64,7 @@
     1.4  
     1.5  (*** Indexing and filtering of theorems ***)
     1.6  
     1.7 -fun eq_brl ((b1,th1),(b2,th2)) = b1=b2 andalso Drule.eq_thm_prop (th1,th2);
     1.8 +fun eq_brl ((b1 : bool, th1), (b2, th2)) = b1 = b2 andalso Drule.eq_thm_prop (th1, th2);
     1.9  
    1.10  (*insert a thm in a discrimination net by its lhs*)
    1.11  fun lhs_insert_thm (th,net) =
    1.12 @@ -155,25 +155,25 @@
    1.13  
    1.14  (*ccs contains the names of the constants possessing congruence rules*)
    1.15  fun add_hidden_vars ccs =
    1.16 -  let fun add_hvars(tm,hvars) = case tm of
    1.17 +  let fun add_hvars tm hvars = case tm of
    1.18                Abs(_,_,body) => add_term_vars(body,hvars)
    1.19              | _$_ => let val (f,args) = strip_comb tm 
    1.20                       in case f of
    1.21                              Const(c,T) => 
    1.22 -                                if c mem ccs
    1.23 -                                then foldr add_hvars hvars args
    1.24 -                                else add_term_vars(tm,hvars)
    1.25 -                          | _ => add_term_vars(tm,hvars)
    1.26 +                                if member (op =) ccs c
    1.27 +                                then fold_rev add_hvars args hvars
    1.28 +                                else add_term_vars (tm, hvars)
    1.29 +                          | _ => add_term_vars (tm, hvars)
    1.30                       end
    1.31              | _ => hvars;
    1.32    in add_hvars end;
    1.33  
    1.34  fun add_new_asm_vars new_asms =
    1.35 -    let fun itf((tm,at),vars) =
    1.36 +    let fun itf (tm, at) vars =
    1.37                  if at then vars else add_term_vars(tm,vars)
    1.38          fun add_list(tm,al,vars) = let val (_,tml) = strip_comb tm
    1.39                  in if length(tml)=length(al)
    1.40 -                   then foldr itf vars (tml~~al)
    1.41 +                   then fold_rev itf (tml ~~ al) vars
    1.42                     else vars
    1.43                  end
    1.44          fun add_vars (tm,vars) = case tm of
    1.45 @@ -194,12 +194,12 @@
    1.46      val lhs = rhs_of_eq 1 thm'
    1.47      val rhs = lhs_of_eq nops thm'
    1.48      val asms = tl(rev(tl(prems_of thm')))
    1.49 -    val hvars = foldr (add_hidden_vars ccs) [] (lhs::rhs::asms)
    1.50 +    val hvars = fold_rev (add_hidden_vars ccs) (lhs::rhs::asms) []
    1.51      val hvars = add_new_asm_vars new_asms (rhs,hvars)
    1.52 -    fun it_asms (asm,hvars) =
    1.53 +    fun it_asms asm hvars =
    1.54          if atomic asm then add_new_asm_vars new_asms (asm,hvars)
    1.55          else add_term_frees(asm,hvars)
    1.56 -    val hvars = foldr it_asms hvars asms
    1.57 +    val hvars = fold_rev it_asms asms hvars
    1.58      val hvs = map (#1 o dest_Var) hvars
    1.59      val refl1_tac = refl_tac 1
    1.60      fun norm_step_tac st = st |>
    1.61 @@ -247,18 +247,18 @@
    1.62  (** Insertion of congruences and rewrites **)
    1.63  
    1.64  (*insert a thm in a thm net*)
    1.65 -fun insert_thm_warn (th,net) = 
    1.66 +fun insert_thm_warn th net = 
    1.67    Net.insert_term Drule.eq_thm_prop (concl_of th, th) net
    1.68    handle Net.INSERT => 
    1.69      (writeln"\nDuplicate rewrite or congruence rule:"; print_thm th;
    1.70       net);
    1.71  
    1.72 -val insert_thms = foldr insert_thm_warn;
    1.73 +val insert_thms = fold_rev insert_thm_warn;
    1.74  
    1.75  fun addrew(SS{auto_tac,congs,cong_net,mk_simps,simps,simp_net}, thm) =
    1.76  let val thms = mk_simps thm
    1.77  in SS{auto_tac=auto_tac,congs=congs, cong_net=cong_net, mk_simps=mk_simps,
    1.78 -      simps = (thm,thms)::simps, simp_net = insert_thms simp_net thms}
    1.79 +      simps = (thm,thms)::simps, simp_net = insert_thms thms simp_net}
    1.80  end;
    1.81  
    1.82  val op addrews = Library.foldl addrew;
    1.83 @@ -266,25 +266,25 @@
    1.84  fun op addcongs(SS{auto_tac,congs,cong_net,mk_simps,simps,simp_net}, thms) =
    1.85  let val congs' = thms @ congs;
    1.86  in SS{auto_tac=auto_tac, congs= congs',
    1.87 -      cong_net= insert_thms cong_net (map mk_trans thms),
    1.88 +      cong_net= insert_thms (map mk_trans thms) cong_net,
    1.89        mk_simps= normed_rews congs', simps=simps, simp_net=simp_net}
    1.90  end;
    1.91  
    1.92  (** Deletion of congruences and rewrites **)
    1.93  
    1.94  (*delete a thm from a thm net*)
    1.95 -fun delete_thm_warn (th,net) = 
    1.96 +fun delete_thm_warn th net = 
    1.97    Net.delete_term Drule.eq_thm_prop (concl_of th, th) net
    1.98    handle Net.DELETE => 
    1.99      (writeln"\nNo such rewrite or congruence rule:";  print_thm th;
   1.100       net);
   1.101  
   1.102 -val delete_thms = foldr delete_thm_warn;
   1.103 +val delete_thms = fold_rev delete_thm_warn;
   1.104  
   1.105  fun op delcongs(SS{auto_tac,congs,cong_net,mk_simps,simps,simp_net}, thms) =
   1.106  let val congs' = fold (remove Drule.eq_thm_prop) thms congs
   1.107  in SS{auto_tac=auto_tac, congs= congs',
   1.108 -      cong_net= delete_thms cong_net (map mk_trans thms),
   1.109 +      cong_net= delete_thms (map mk_trans thms) cong_net,
   1.110        mk_simps= normed_rews congs', simps=simps, simp_net=simp_net}
   1.111  end;
   1.112  
   1.113 @@ -296,7 +296,7 @@
   1.114                             ([],simps'))
   1.115      val (thms,simps') = find(simps,[])
   1.116  in SS{auto_tac=auto_tac, congs=congs, cong_net=cong_net, mk_simps=mk_simps,
   1.117 -      simps = simps', simp_net = delete_thms simp_net thms}
   1.118 +      simps = simps', simp_net = delete_thms thms simp_net }
   1.119  end;
   1.120  
   1.121  val op delrews = Library.foldl delrew;
     2.1 --- a/src/HOL/Import/replay.ML	Fri Oct 20 17:07:25 2006 +0200
     2.2 +++ b/src/HOL/Import/replay.ML	Fri Oct 20 17:07:26 2006 +0200
     2.3 @@ -27,12 +27,12 @@
     2.4  	    end
     2.5  	  | rp (PSubst(prfs,ctxt,prf)) thy =
     2.6  	    let
     2.7 -		val (thy',ths) = foldr (fn (p,(thy,ths)) =>
     2.8 +		val (thy',ths) = fold_rev (fn p => fn (thy, ths) =>
     2.9  					   let
    2.10  					       val (thy',th) = rp' p thy
    2.11  					   in
    2.12  					       (thy',th::ths)
    2.13 -					   end) (thy,[]) prfs
    2.14 +					   end) prfs (thy,[])
    2.15  		val (thy'',th) = rp' prf thy'
    2.16  	    in
    2.17  		P.SUBST ths ctxt th thy''
     3.1 --- a/src/HOL/Import/shuffler.ML	Fri Oct 20 17:07:25 2006 +0200
     3.2 +++ b/src/HOL/Import/shuffler.ML	Fri Oct 20 17:07:26 2006 +0200
     3.3 @@ -83,7 +83,7 @@
     3.4  val copy = I
     3.5  val extend = I
     3.6  fun merge _ = Library.gen_union Thm.eq_thm
     3.7 -fun print sg thms =
     3.8 +fun print _ thms =
     3.9      Pretty.writeln (Pretty.big_list "Shuffle theorems:"
    3.10  				    (map Display.pretty_thm thms))
    3.11  end
    3.12 @@ -92,7 +92,7 @@
    3.13  
    3.14  val weaken =
    3.15      let
    3.16 -	val cert = cterm_of (sign_of ProtoPure.thy)
    3.17 +	val cert = cterm_of ProtoPure.thy
    3.18  	val P = Free("P",propT)
    3.19  	val Q = Free("Q",propT)
    3.20  	val PQ = Logic.mk_implies(P,Q)
    3.21 @@ -111,7 +111,7 @@
    3.22  
    3.23  val imp_comm =
    3.24      let
    3.25 -	val cert = cterm_of (sign_of ProtoPure.thy)
    3.26 +	val cert = cterm_of ProtoPure.thy
    3.27  	val P = Free("P",propT)
    3.28  	val Q = Free("Q",propT)
    3.29  	val R = Free("R",propT)
    3.30 @@ -131,7 +131,7 @@
    3.31  
    3.32  val def_norm =
    3.33      let
    3.34 -	val cert = cterm_of (sign_of ProtoPure.thy)
    3.35 +	val cert = cterm_of ProtoPure.thy
    3.36  	val aT = TFree("'a",[])
    3.37  	val bT = TFree("'b",[])
    3.38  	val v = Free("v",aT)
    3.39 @@ -158,7 +158,7 @@
    3.40  
    3.41  val all_comm =
    3.42      let
    3.43 -	val cert = cterm_of (sign_of ProtoPure.thy)
    3.44 +	val cert = cterm_of ProtoPure.thy
    3.45  	val xT = TFree("'a",[])
    3.46  	val yT = TFree("'b",[])
    3.47  	val P = Free("P",xT-->yT-->propT)
    3.48 @@ -182,7 +182,7 @@
    3.49  
    3.50  val equiv_comm =
    3.51      let
    3.52 -	val cert = cterm_of (sign_of ProtoPure.thy)
    3.53 +	val cert = cterm_of ProtoPure.thy
    3.54  	val T    = TFree("'a",[])
    3.55  	val t    = Free("t",T)
    3.56  	val u    = Free("u",T)
    3.57 @@ -216,28 +216,28 @@
    3.58    | swap_bound n (Abs(x,xT,t)) = Abs(x,xT,swap_bound (n+1) t)
    3.59    | swap_bound n t = t
    3.60  
    3.61 -fun rew_th sg (xv as (x,xT)) (yv as (y,yT)) t =
    3.62 +fun rew_th thy (xv as (x,xT)) (yv as (y,yT)) t =
    3.63      let
    3.64  	val lhs = list_all ([xv,yv],t)
    3.65  	val rhs = list_all ([yv,xv],swap_bound 0 t)
    3.66  	val rew = Logic.mk_equals (lhs,rhs)
    3.67 -	val init = trivial (cterm_of sg rew)
    3.68 +	val init = trivial (cterm_of thy rew)
    3.69      in
    3.70  	(all_comm RS init handle e => (message "rew_th"; OldGoals.print_exn e))
    3.71      end
    3.72  
    3.73 -fun quant_rewrite sg assumes (t as Const("all",T1) $ (Abs(x,xT,Const("all",T2) $ Abs(y,yT,body)))) =
    3.74 +fun quant_rewrite thy assumes (t as Const("all",T1) $ (Abs(x,xT,Const("all",T2) $ Abs(y,yT,body)))) =
    3.75      let
    3.76  	val res = (find_bound 0 body;2) handle RESULT i => i
    3.77      in
    3.78  	case res of
    3.79 -	    0 => SOME (rew_th sg (x,xT) (y,yT) body)
    3.80 +	    0 => SOME (rew_th thy (x,xT) (y,yT) body)
    3.81  	  | 1 => if string_ord(y,x) = LESS
    3.82  		 then
    3.83  		     let
    3.84  			 val newt = Const("all",T1) $ (Abs(y,xT,Const("all",T2) $ Abs(x,yT,body)))
    3.85 -			 val t_th    = reflexive (cterm_of sg t)
    3.86 -			 val newt_th = reflexive (cterm_of sg newt)
    3.87 +			 val t_th    = reflexive (cterm_of thy t)
    3.88 +			 val newt_th = reflexive (cterm_of thy newt)
    3.89  		     in
    3.90  			 SOME (transitive t_th newt_th)
    3.91  		     end
    3.92 @@ -264,10 +264,10 @@
    3.93  		  | _ => error "Internal error in Shuffler.freeze_thaw") type_inst)
    3.94      end
    3.95  
    3.96 -fun inst_tfrees sg [] thm = thm
    3.97 -  | inst_tfrees sg ((name,U)::rest) thm = 
    3.98 +fun inst_tfrees thy [] thm = thm
    3.99 +  | inst_tfrees thy ((name,U)::rest) thm = 
   3.100      let
   3.101 -	val cU = ctyp_of sg U
   3.102 +	val cU = ctyp_of thy U
   3.103  	val tfrees = add_term_tfrees (prop_of thm,[])
   3.104  	val (rens, thm') = Thm.varifyT'
   3.105      (remove (op = o apsnd fst) name tfrees) thm
   3.106 @@ -275,10 +275,10 @@
   3.107  	    case rens of
   3.108  		[] => thm'
   3.109  	      | [((_, S), idx)] => instantiate
   3.110 -            ([(ctyp_of sg (TVar (idx, S)), cU)], []) thm'
   3.111 +            ([(ctyp_of thy (TVar (idx, S)), cU)], []) thm'
   3.112  	      | _ => error "Shuffler.inst_tfrees internal error"
   3.113      in
   3.114 -	inst_tfrees sg rest mid
   3.115 +	inst_tfrees thy rest mid
   3.116      end
   3.117  
   3.118  fun is_Abs (Abs _) = true
   3.119 @@ -295,11 +295,11 @@
   3.120      end
   3.121    | eta_redex _ = false
   3.122  
   3.123 -fun eta_contract sg assumes origt =
   3.124 +fun eta_contract thy assumes origt =
   3.125      let
   3.126  	val (typet,Tinst) = freeze_thaw_term origt
   3.127 -	val (init,thaw) = freeze_thaw (reflexive (cterm_of sg typet))
   3.128 -	val final = inst_tfrees sg Tinst o thaw
   3.129 +	val (init,thaw) = freeze_thaw (reflexive (cterm_of thy typet))
   3.130 +	val final = inst_tfrees thy Tinst o thaw
   3.131  	val t = #1 (Logic.dest_equals (prop_of init))
   3.132  	val _ =
   3.133  	    let
   3.134 @@ -307,11 +307,11 @@
   3.135  	    in
   3.136  		if not (lhs aconv origt)
   3.137  		then (writeln "Something is utterly wrong: (orig,lhs,frozen type,t,tinst)";
   3.138 -		      writeln (string_of_cterm (cterm_of sg origt));
   3.139 -		      writeln (string_of_cterm (cterm_of sg lhs));
   3.140 -		      writeln (string_of_cterm (cterm_of sg typet));
   3.141 -		      writeln (string_of_cterm (cterm_of sg t));
   3.142 -		      app (fn (n,T) => writeln (n ^ ": " ^ (string_of_ctyp (ctyp_of sg T)))) Tinst;
   3.143 +		      writeln (string_of_cterm (cterm_of thy origt));
   3.144 +		      writeln (string_of_cterm (cterm_of thy lhs));
   3.145 +		      writeln (string_of_cterm (cterm_of thy typet));
   3.146 +		      writeln (string_of_cterm (cterm_of thy t));
   3.147 +		      app (fn (n,T) => writeln (n ^ ": " ^ (string_of_ctyp (ctyp_of thy T)))) Tinst;
   3.148  		      writeln "done")
   3.149  		else ()
   3.150  	    end
   3.151 @@ -321,7 +321,7 @@
   3.152  	    ((if eta_redex P andalso eta_redex Q
   3.153  	      then
   3.154  		  let
   3.155 -		      val cert = cterm_of sg
   3.156 +		      val cert = cterm_of thy
   3.157  		      val v = Free(Name.variant (add_term_free_names(t,[])) "v",xT)
   3.158  		      val cv = cert v
   3.159  		      val ct = cert t
   3.160 @@ -347,21 +347,21 @@
   3.161  	  | _ => NONE
   3.162         end
   3.163  
   3.164 -fun beta_fun sg assume t =
   3.165 -    SOME (beta_conversion true (cterm_of sg t))
   3.166 +fun beta_fun thy assume t =
   3.167 +    SOME (beta_conversion true (cterm_of thy t))
   3.168  
   3.169  val meta_sym_rew = thm "refl"
   3.170  
   3.171 -fun equals_fun sg assume t =
   3.172 +fun equals_fun thy assume t =
   3.173      case t of
   3.174  	Const("op ==",_) $ u $ v => if Term.term_ord (u,v) = LESS then SOME (meta_sym_rew) else NONE
   3.175        | _ => NONE
   3.176  
   3.177 -fun eta_expand sg assumes origt =
   3.178 +fun eta_expand thy assumes origt =
   3.179      let
   3.180  	val (typet,Tinst) = freeze_thaw_term origt
   3.181 -	val (init,thaw) = freeze_thaw (reflexive (cterm_of sg typet))
   3.182 -	val final = inst_tfrees sg Tinst o thaw
   3.183 +	val (init,thaw) = freeze_thaw (reflexive (cterm_of thy typet))
   3.184 +	val final = inst_tfrees thy Tinst o thaw
   3.185  	val t = #1 (Logic.dest_equals (prop_of init))
   3.186  	val _ =
   3.187  	    let
   3.188 @@ -369,11 +369,11 @@
   3.189  	    in
   3.190  		if not (lhs aconv origt)
   3.191  		then (writeln "Something is utterly wrong: (orig,lhs,frozen type,t,tinst)";
   3.192 -		      writeln (string_of_cterm (cterm_of sg origt));
   3.193 -		      writeln (string_of_cterm (cterm_of sg lhs));
   3.194 -		      writeln (string_of_cterm (cterm_of sg typet));
   3.195 -		      writeln (string_of_cterm (cterm_of sg t));
   3.196 -		      app (fn (n,T) => writeln (n ^ ": " ^ (string_of_ctyp (ctyp_of sg T)))) Tinst;
   3.197 +		      writeln (string_of_cterm (cterm_of thy origt));
   3.198 +		      writeln (string_of_cterm (cterm_of thy lhs));
   3.199 +		      writeln (string_of_cterm (cterm_of thy typet));
   3.200 +		      writeln (string_of_cterm (cterm_of thy t));
   3.201 +		      app (fn (n,T) => writeln (n ^ ": " ^ (string_of_ctyp (ctyp_of thy T)))) Tinst;
   3.202  		      writeln "done")
   3.203  		else ()
   3.204  	    end
   3.205 @@ -384,7 +384,7 @@
   3.206  	    then (case domain_type T of
   3.207  		      Type("fun",[aT,bT]) =>
   3.208  		      let
   3.209 -			  val cert = cterm_of sg
   3.210 +			  val cert = cterm_of thy
   3.211  			  val vname = Name.variant (add_term_free_names(t,[])) "v"
   3.212  			  val v = Free(vname,aT)
   3.213  			  val cv = cert v
   3.214 @@ -409,7 +409,7 @@
   3.215  		      end
   3.216  		    | _ => NONE)
   3.217  	    else NONE
   3.218 -	  | _ => (error ("Bad eta_expand argument" ^ (string_of_cterm (cterm_of sg t))); NONE)
   3.219 +	  | _ => (error ("Bad eta_expand argument" ^ (string_of_cterm (cterm_of thy t))); NONE)
   3.220      end
   3.221      handle e => (writeln "eta_expand internal error"; OldGoals.print_exn e)
   3.222  
   3.223 @@ -423,30 +423,30 @@
   3.224  val S  = mk_free "S" xT
   3.225  val S'  = mk_free "S'" xT
   3.226  in
   3.227 -fun beta_simproc sg = Simplifier.simproc_i
   3.228 -		      sg
   3.229 +fun beta_simproc thy = Simplifier.simproc_i
   3.230 +		      thy
   3.231  		      "Beta-contraction"
   3.232  		      [Abs("x",xT,Q) $ S]
   3.233  		      beta_fun
   3.234  
   3.235 -fun equals_simproc sg = Simplifier.simproc_i
   3.236 -		      sg
   3.237 +fun equals_simproc thy = Simplifier.simproc_i
   3.238 +		      thy
   3.239  		      "Ordered rewriting of meta equalities"
   3.240  		      [Const("op ==",xT) $ S $ S']
   3.241  		      equals_fun
   3.242  
   3.243 -fun quant_simproc sg = Simplifier.simproc_i
   3.244 -			   sg
   3.245 +fun quant_simproc thy = Simplifier.simproc_i
   3.246 +			   thy
   3.247  			   "Ordered rewriting of nested quantifiers"
   3.248  			   [all xT $ (Abs("x",xT,all yT $ (Abs("y",yT,P $ Bound 1 $ Bound 0))))]
   3.249  			   quant_rewrite
   3.250 -fun eta_expand_simproc sg = Simplifier.simproc_i
   3.251 -			 sg
   3.252 +fun eta_expand_simproc thy = Simplifier.simproc_i
   3.253 +			 thy
   3.254  			 "Smart eta-expansion by equivalences"
   3.255  			 [Logic.mk_equals(Q,R)]
   3.256  			 eta_expand
   3.257 -fun eta_contract_simproc sg = Simplifier.simproc_i
   3.258 -			 sg
   3.259 +fun eta_contract_simproc thy = Simplifier.simproc_i
   3.260 +			 thy
   3.261  			 "Smart handling of eta-contractions"
   3.262  			 [all xT $ (Abs("x",xT,Logic.mk_equals(Q $ Bound 0,R $ Bound 0)))]
   3.263  			 eta_contract
   3.264 @@ -455,7 +455,7 @@
   3.265  (* Disambiguates the names of bound variables in a term, returning t
   3.266  == t' where all the names of bound variables in t' are unique *)
   3.267  
   3.268 -fun disamb_bound sg t =
   3.269 +fun disamb_bound thy t =
   3.270      let
   3.271  	
   3.272  	fun F (t $ u,idx) =
   3.273 @@ -474,8 +474,8 @@
   3.274  	    end
   3.275  	  | F arg = arg
   3.276  	val (t',_) = F (t,0)
   3.277 -	val ct = cterm_of sg t
   3.278 -	val ct' = cterm_of sg t'
   3.279 +	val ct = cterm_of thy t
   3.280 +	val ct' = cterm_of thy t'
   3.281  	val res = transitive (reflexive ct) (reflexive ct')
   3.282  	val _ = message ("disamb_term: " ^ (string_of_thm res))
   3.283      in
   3.284 @@ -488,12 +488,11 @@
   3.285  
   3.286  fun norm_term thy t =
   3.287      let
   3.288 -	val sg = sign_of thy
   3.289  	val norms = ShuffleData.get thy
   3.290  	val ss = Simplifier.theory_context thy empty_ss
   3.291            setmksimps single
   3.292 -	  addsimps (map (Thm.transfer sg) norms)
   3.293 -          addsimprocs [quant_simproc sg, eta_expand_simproc sg,eta_contract_simproc sg]
   3.294 +	  addsimps (map (Thm.transfer thy) norms)
   3.295 +          addsimprocs [quant_simproc thy, eta_expand_simproc thy,eta_contract_simproc thy]
   3.296  	fun chain f th =
   3.297  	    let
   3.298                  val rhs = snd (dest_equals (cprop_of th))
   3.299 @@ -501,7 +500,7 @@
   3.300  		transitive th (f rhs)
   3.301  	    end
   3.302  	val th =
   3.303 -            t |> disamb_bound sg
   3.304 +            t |> disamb_bound thy
   3.305  	      |> chain (Simplifier.full_rewrite ss)
   3.306                |> chain eta_conversion
   3.307  	      |> strip_shyps
   3.308 @@ -509,7 +508,7 @@
   3.309      in
   3.310  	th
   3.311      end
   3.312 -    handle e => (writeln "norm_term internal error"; print_sign_exn (sign_of thy) e)
   3.313 +    handle e => (writeln "norm_term internal error"; print_sign_exn thy e)
   3.314  
   3.315  
   3.316  (* Closes a theorem with respect to free and schematic variables (does
   3.317 @@ -517,11 +516,11 @@
   3.318  
   3.319  fun close_thm th =
   3.320      let
   3.321 -	val sg = sign_of_thm th
   3.322 +	val thy = sign_of_thm th
   3.323  	val c = prop_of th
   3.324  	val vars = add_term_frees (c,add_term_vars(c,[]))
   3.325      in
   3.326 -	Drule.forall_intr_list (map (cterm_of sg) vars) th
   3.327 +	Drule.forall_intr_list (map (cterm_of thy) vars) th
   3.328      end
   3.329      handle e => (writeln "close_thm internal error"; OldGoals.print_exn e)
   3.330  
   3.331 @@ -534,14 +533,14 @@
   3.332  	equal_elim (norm_term thy c) th
   3.333      end
   3.334  
   3.335 -(* make_equal sg t u tries to construct the theorem t == u under the
   3.336 -signature sg.  If it succeeds, SOME (t == u) is returned, otherwise
   3.337 +(* make_equal thy t u tries to construct the theorem t == u under the
   3.338 +signature thy.  If it succeeds, SOME (t == u) is returned, otherwise
   3.339  NONE is returned. *)
   3.340  
   3.341 -fun make_equal sg t u =
   3.342 +fun make_equal thy t u =
   3.343      let
   3.344 -	val t_is_t' = norm_term sg t
   3.345 -	val u_is_u' = norm_term sg u
   3.346 +	val t_is_t' = norm_term thy t
   3.347 +	val u_is_u' = norm_term thy u
   3.348  	val th = transitive t_is_t' (symmetric u_is_u')
   3.349  	val _ = message ("make_equal: SOME " ^ (string_of_thm th))
   3.350      in
   3.351 @@ -569,7 +568,7 @@
   3.352      end
   3.353      
   3.354  val collect_ignored =
   3.355 -    foldr (fn (thm,cs) =>
   3.356 +    fold_rev (fn thm => fn cs =>
   3.357  	      let
   3.358  		  val (lhs,rhs) = Logic.dest_equals (prop_of thm)
   3.359  		  val ignore_lhs = term_consts lhs \\ term_consts rhs
   3.360 @@ -584,10 +583,9 @@
   3.361  
   3.362  fun set_prop thy t =
   3.363      let
   3.364 -	val sg = sign_of thy
   3.365  	val vars = add_term_frees (t,add_term_vars (t,[]))
   3.366 -	val closed_t = foldr (fn (v,body) => let val vT = type_of v
   3.367 -					     in all vT $ (Abs("x",vT,abstract_over(v,body))) end) t vars
   3.368 +	val closed_t = Library.foldr (fn (v, body) =>
   3.369 +      let val vT = type_of v in all vT $ (Abs ("x", vT, abstract_over (v, body))) end) (vars, t)
   3.370  	val rew_th = norm_term thy closed_t
   3.371  	val rhs = snd (dest_equals (cprop_of rew_th))
   3.372  
   3.373 @@ -595,7 +593,7 @@
   3.374  	fun process [] = NONE
   3.375  	  | process ((name,th)::thms) =
   3.376  	    let
   3.377 -		val norm_th = Thm.varifyT (norm_thm thy (close_thm (Thm.transfer sg th)))
   3.378 +		val norm_th = Thm.varifyT (norm_thm thy (close_thm (Thm.transfer thy th)))
   3.379  		val triv_th = trivial rhs
   3.380  		val _ = message ("Shuffler.set_prop: Gluing together " ^ (string_of_thm norm_th) ^ " and " ^ (string_of_thm triv_th))
   3.381  		val mod_th = case Seq.pull (bicompose false (*true*) (false,norm_th,0) 1 triv_th) of
   3.382 @@ -608,7 +606,7 @@
   3.383  			val closed_th = equal_elim (symmetric rew_th) mod_th
   3.384  		    in
   3.385  			message ("Shuffler.set_prop succeeded by " ^ name);
   3.386 -			SOME (name,forall_elim_list (map (cterm_of sg) vars) closed_th)
   3.387 +			SOME (name,forall_elim_list (map (cterm_of thy) vars) closed_th)
   3.388  		    end
   3.389  		  | NONE => process thms
   3.390  	    end
   3.391 @@ -626,7 +624,7 @@
   3.392  fun find_potential thy t =
   3.393      let
   3.394  	val shuffles = ShuffleData.get thy
   3.395 -	val ignored = collect_ignored [] shuffles
   3.396 +	val ignored = collect_ignored shuffles []
   3.397  	val rel_consts = term_consts t \\ ignored
   3.398  	val pot_thms = PureThy.thms_containing_consts thy rel_consts
   3.399      in
     4.1 --- a/src/HOL/Integ/cooper_dec.ML	Fri Oct 20 17:07:25 2006 +0200
     4.2 +++ b/src/HOL/Integ/cooper_dec.ML	Fri Oct 20 17:07:26 2006 +0200
     4.3 @@ -443,7 +443,7 @@
     4.4     val ts = coeffs_of t
     4.5     in case ts of
     4.6       [] => raise DVD_UNKNOWN
     4.7 -    |_  => foldr (fn(k,r) => r andalso (k mod dn = 0)) true ts
     4.8 +    |_  => fold_rev (fn k => fn r => r andalso (k mod dn = 0)) ts true
     4.9     end;
    4.10  
    4.11  
    4.12 @@ -736,7 +736,7 @@
    4.13               in (rw,HOLogic.mk_disj(F',rf)) 
    4.14  	     end)
    4.15      val f = if b then linear_add else linear_sub
    4.16 -    val p_elements = foldr (fn (i,l) => l union (map (fn e => f [] e (mk_numeral i)) st)) [] (myupto 1 d)
    4.17 +    val p_elements = fold_rev (fn i => fn l => l union (map (fn e => f [] e (mk_numeral i)) st)) (myupto 1 d) []
    4.18      in h p_elements
    4.19      end;
    4.20  
     5.1 --- a/src/HOL/Nominal/nominal_permeq.ML	Fri Oct 20 17:07:25 2006 +0200
     5.2 +++ b/src/HOL/Nominal/nominal_permeq.ML	Fri Oct 20 17:07:26 2006 +0200
     5.3 @@ -268,9 +268,9 @@
     5.4              val ps = Logic.strip_params (term_of goal);
     5.5              val Ts = rev (map snd ps);
     5.6              val vs = collect_vars 0 x [];
     5.7 -            val s = foldr (fn (v, s) =>
     5.8 +            val s = Library.foldr (fn (v, s) =>
     5.9                  HOLogic.pair_const (fastype_of1 (Ts, v)) (fastype_of1 (Ts, s)) $ v $ s)
    5.10 -              HOLogic.unit vs;
    5.11 +              (vs, HOLogic.unit);
    5.12              val s' = list_abs (ps,
    5.13                Const ("Nominal.supp", fastype_of1 (Ts, s) --> body_type T) $ s);
    5.14              val supports_rule' = Thm.lift_rule goal supports_rule;
    5.15 @@ -305,9 +305,9 @@
    5.16              val ps = Logic.strip_params (term_of goal);
    5.17              val Ts = rev (map snd ps);
    5.18              val vs = collect_vars 0 t [];
    5.19 -            val s = foldr (fn (v, s) =>
    5.20 +            val s = Library.foldr (fn (v, s) =>
    5.21                  HOLogic.pair_const (fastype_of1 (Ts, v)) (fastype_of1 (Ts, s)) $ v $ s)
    5.22 -              HOLogic.unit vs;
    5.23 +              (vs, HOLogic.unit);
    5.24              val s' = list_abs (ps,
    5.25                Const ("Nominal.supp", fastype_of1 (Ts, s) --> (HOLogic.mk_setT T)) $ s);
    5.26              val supports_fresh_rule' = Thm.lift_rule goal supports_fresh_rule;
     6.1 --- a/src/HOL/Real/ferrante_rackoff.ML	Fri Oct 20 17:07:25 2006 +0200
     6.2 +++ b/src/HOL/Real/ferrante_rackoff.ML	Fri Oct 20 17:07:26 2006 +0200
     6.3 @@ -5,94 +5,85 @@
     6.4  Ferrante and Rackoff Algorithm.
     6.5  *)
     6.6  
     6.7 -structure Ferrante_Rackoff:
     6.8 +signature FERRANTE_RACKOFF =
     6.9  sig
    6.10 -  val trace : bool ref
    6.11 -  val ferrack_tac : bool -> int -> tactic
    6.12 -  val setup : theory -> theory
    6.13 -end =
    6.14 +  val ferrack_tac: bool -> int -> tactic
    6.15 +  val setup: theory -> theory
    6.16 +  val trace: bool ref
    6.17 +end;
    6.18 +
    6.19 +structure Ferrante_Rackoff : FERRANTE_RACKOFF =
    6.20  struct
    6.21  
    6.22  val trace = ref false;
    6.23  fun trace_msg s = if !trace then tracing s else ();
    6.24  
    6.25 -val context_ss = simpset_of (the_context ());
    6.26 -
    6.27 -val nT = HOLogic.natT;
    6.28 -val binarith = map thm
    6.29 -  ["Pls_0_eq", "Min_1_eq",
    6.30 - "pred_Pls","pred_Min","pred_1","pred_0",
    6.31 +val binarith = map thm ["Pls_0_eq", "Min_1_eq", "pred_Pls", "pred_Min","pred_1","pred_0",
    6.32    "succ_Pls", "succ_Min", "succ_1", "succ_0",
    6.33 -  "add_Pls", "add_Min", "add_BIT_0", "add_BIT_10",
    6.34 -  "add_BIT_11", "minus_Pls", "minus_Min", "minus_1", 
    6.35 -  "minus_0", "mult_Pls", "mult_Min", "mult_1", "mult_0", 
    6.36 +  "add_Pls", "add_Min", "add_BIT_0", "add_BIT_10", "add_BIT_11",
    6.37 +  "minus_Pls", "minus_Min", "minus_1", "minus_0",
    6.38 +  "mult_Pls", "mult_Min", "mult_1", "mult_0", 
    6.39    "add_Pls_right", "add_Min_right"];
    6.40 - val intarithrel = 
    6.41 -     (map thm ["int_eq_number_of_eq","int_neg_number_of_BIT", 
    6.42 -		"int_le_number_of_eq","int_iszero_number_of_0",
    6.43 -		"int_less_number_of_eq_neg"]) @
    6.44 -     (map (fn s => thm s RS thm "lift_bool") 
    6.45 -	  ["int_iszero_number_of_Pls","int_iszero_number_of_1",
    6.46 -	   "int_neg_number_of_Min"])@
    6.47 -     (map (fn s => thm s RS thm "nlift_bool") 
    6.48 -	  ["int_nonzero_number_of_Min","int_not_neg_number_of_Pls"]);
    6.49 -     
    6.50 +
    6.51 +val intarithrel = 
    6.52 +  map thm ["int_eq_number_of_eq", "int_neg_number_of_BIT", "int_le_number_of_eq",
    6.53 +    "int_iszero_number_of_0", "int_less_number_of_eq_neg"]
    6.54 +  @ map (fn s => thm s RS thm "lift_bool") ["int_iszero_number_of_Pls",
    6.55 +    "int_iszero_number_of_1", "int_neg_number_of_Min"]
    6.56 +  @ map (fn s => thm s RS thm "nlift_bool") ["int_nonzero_number_of_Min",
    6.57 +    "int_not_neg_number_of_Pls"];
    6.58 + 
    6.59  val intarith = map thm ["int_number_of_add_sym", "int_number_of_minus_sym",
    6.60 -			"int_number_of_diff_sym", "int_number_of_mult_sym"];
    6.61 +  "int_number_of_diff_sym", "int_number_of_mult_sym"];
    6.62 +
    6.63  val natarith = map thm ["add_nat_number_of", "diff_nat_number_of",
    6.64 -			"mult_nat_number_of", "eq_nat_number_of",
    6.65 -			"less_nat_number_of"]
    6.66 -val powerarith = 
    6.67 -    (map thm ["nat_number_of", "zpower_number_of_even", 
    6.68 -	      "zpower_Pls", "zpower_Min"]) @ 
    6.69 -    [(Tactic.simplify true [thm "zero_eq_Numeral0_nring", 
    6.70 -			   thm "one_eq_Numeral1_nring"] 
    6.71 -  (thm "zpower_number_of_odd"))]
    6.72 +  "mult_nat_number_of", "eq_nat_number_of", "less_nat_number_of"];
    6.73 +
    6.74 +val powerarith =
    6.75 +  map thm ["nat_number_of", "zpower_number_of_even",
    6.76 +  "zpower_Pls", "zpower_Min"]
    6.77 +  @ [Tactic.simplify true [thm "zero_eq_Numeral0_nring", thm "one_eq_Numeral1_nring"]
    6.78 +    (thm "zpower_number_of_odd")]
    6.79  
    6.80  val comp_arith = binarith @ intarith @ intarithrel @ natarith 
    6.81 -	    @ powerarith @[thm"not_false_eq_true", thm "not_true_eq_false"];
    6.82 +  @ powerarith @ [thm "not_false_eq_true", thm "not_true_eq_false"];
    6.83  
    6.84 -fun prepare_for_linr sg q fm = 
    6.85 +fun prepare_for_linr q fm = 
    6.86    let
    6.87      val ps = Logic.strip_params fm
    6.88      val hs = map HOLogic.dest_Trueprop (Logic.strip_assums_hyp fm)
    6.89      val c = HOLogic.dest_Trueprop (Logic.strip_assums_concl fm)
    6.90 -    fun mk_all ((s, T), (P,n)) =
    6.91 +    fun mk_all ((s, T), (P, n)) =
    6.92        if 0 mem loose_bnos P then
    6.93          (HOLogic.all_const T $ Abs (s, T, P), n)
    6.94        else (incr_boundvars ~1 P, n-1)
    6.95      fun mk_all2 (v, t) = HOLogic.all_const (fastype_of v) $ lambda v t;
    6.96 -      val rhs = hs
    6.97 -(*    val (rhs,irhs) = List.partition (relevant (rev ps)) hs *)
    6.98 -    val np = length ps
    6.99 -    val (fm',np) =  foldr (fn ((x, T), (fm,n)) => mk_all ((x, T), (fm,n)))
   6.100 -      (foldr HOLogic.mk_imp c rhs, np) ps
   6.101 -    val (vs, _) = List.partition (fn t => q orelse (type_of t) = nT)
   6.102 +    val rhs = hs;
   6.103 +    val np = length ps;
   6.104 +    val (fm', np) = Library.foldr mk_all (ps, (Library.foldr HOLogic.mk_imp (rhs, c), np));
   6.105 +    val (vs, _) = List.partition (fn t => q orelse (type_of t) = HOLogic.natT)
   6.106        (term_frees fm' @ term_vars fm');
   6.107 -    val fm2 = foldr mk_all2 fm' vs
   6.108 +    val fm2 = Library.foldr mk_all2 (vs, fm');
   6.109    in (fm2, np + length vs, length rhs) end;
   6.110  
   6.111 -(*Object quantifier to meta --*)
   6.112 -fun spec_step n th = if (n=0) then th else (spec_step (n-1) th) RS spec ;
   6.113 -
   6.114 -(* object implication to meta---*)
   6.115 -fun mp_step n th = if (n=0) then th else (mp_step (n-1) th) RS mp;
   6.116 -
   6.117 +fun spec_step n th = if n = 0 then th else spec_step (n - 1) th RS spec ;
   6.118 +fun mp_step n th = if n = 0 then th else mp_step (n - 1) th RS mp;
   6.119  
   6.120 -fun ferrack_tac q i = 
   6.121 -    (ObjectLogic.atomize_tac i) 
   6.122 -	THEN (REPEAT_DETERM (split_tac [split_min, split_max,abs_split] i))
   6.123 -	THEN (fn st =>
   6.124 +local
   6.125 +  val context_ss = simpset_of (the_context ())
   6.126 +in fun ferrack_tac q i =  ObjectLogic.atomize_tac i
   6.127 +  THEN REPEAT_DETERM (split_tac [split_min, split_max,abs_split] i)
   6.128 +  THEN (fn st =>
   6.129    let
   6.130 -    val g = List.nth (prems_of st, i - 1)
   6.131 -    val sg = sign_of_thm st
   6.132 +    val g = nth (prems_of st) (i - 1)
   6.133 +    val thy = sign_of_thm st
   6.134      (* Transform the term*)
   6.135 -    val (t,np,nh) = prepare_for_linr sg q g
   6.136 +    val (t,np,nh) = prepare_for_linr q g
   6.137      (* Some simpsets for dealing with mod div abs and nat*)
   6.138      val simpset0 = HOL_basic_ss addsimps comp_arith addsplits [split_min, split_max]
   6.139      (* simp rules for elimination of abs *)
   6.140      val simpset3 = HOL_basic_ss addsplits [abs_split]
   6.141 -    val ct = cterm_of sg (HOLogic.mk_Trueprop t)
   6.142 +    val ct = cterm_of thy (HOLogic.mk_Trueprop t)
   6.143      (* Theorem for the nat --> int transformation *)
   6.144      val pre_thm = Seq.hd (EVERY
   6.145        [simp_tac simpset0 1, TRY (simp_tac context_ss 1)]
   6.146 @@ -101,10 +92,10 @@
   6.147      (* The result of the quantifier elimination *)
   6.148      val (th, tac) = case (prop_of pre_thm) of
   6.149          Const ("==>", _) $ (Const ("Trueprop", _) $ t1) $ _ =>
   6.150 -    let val pth = Ferrante_Rackoff_Proof.qelim (cterm_of sg (Pattern.eta_long [] t1))
   6.151 +    let val pth = Ferrante_Rackoff_Proof.qelim (cterm_of thy (Pattern.eta_long [] t1))
   6.152      in 
   6.153            (trace_msg ("calling procedure with term:\n" ^
   6.154 -             Sign.string_of_term sg t1);
   6.155 +             Sign.string_of_term thy t1);
   6.156             ((pth RS iffD2) RS pre_thm,
   6.157              assm_tac (i + 1) THEN (if q then I else TRY) (rtac TrueI i)))
   6.158      end
   6.159 @@ -112,10 +103,11 @@
   6.160    in (rtac (((mp_step nh) o (spec_step np)) th) i 
   6.161        THEN tac) st
   6.162    end handle Subscript => no_tac st | Ferrante_Rackoff_Proof.FAILURE _ => no_tac st);
   6.163 +end; (*local*)
   6.164  
   6.165  fun ferrack_args meth =
   6.166 - let val parse_flag = 
   6.167 -         Args.$$$ "no_quantify" >> (K (K false));
   6.168 + let
   6.169 +   val parse_flag =  Args.$$$ "no_quantify" >> (K (K false));
   6.170   in
   6.171     Method.simple_args 
   6.172    (Scan.optional (Args.$$$ "(" |-- Scan.repeat1 parse_flag --| Args.$$$ ")") [] >>
     7.1 --- a/src/HOL/Tools/Presburger/cooper_dec.ML	Fri Oct 20 17:07:25 2006 +0200
     7.2 +++ b/src/HOL/Tools/Presburger/cooper_dec.ML	Fri Oct 20 17:07:26 2006 +0200
     7.3 @@ -443,7 +443,7 @@
     7.4     val ts = coeffs_of t
     7.5     in case ts of
     7.6       [] => raise DVD_UNKNOWN
     7.7 -    |_  => foldr (fn(k,r) => r andalso (k mod dn = 0)) true ts
     7.8 +    |_  => fold_rev (fn k => fn r => r andalso (k mod dn = 0)) ts true
     7.9     end;
    7.10  
    7.11  
    7.12 @@ -736,7 +736,7 @@
    7.13               in (rw,HOLogic.mk_disj(F',rf)) 
    7.14  	     end)
    7.15      val f = if b then linear_add else linear_sub
    7.16 -    val p_elements = foldr (fn (i,l) => l union (map (fn e => f [] e (mk_numeral i)) st)) [] (myupto 1 d)
    7.17 +    val p_elements = fold_rev (fn i => fn l => l union (map (fn e => f [] e (mk_numeral i)) st)) (myupto 1 d) []
    7.18      in h p_elements
    7.19      end;
    7.20  
     8.1 --- a/src/HOL/Tools/datatype_prop.ML	Fri Oct 20 17:07:25 2006 +0200
     8.2 +++ b/src/HOL/Tools/datatype_prop.ML	Fri Oct 20 17:07:26 2006 +0200
     8.3 @@ -64,24 +64,23 @@
     8.4  
     8.5  fun make_injs descr sorts =
     8.6    let
     8.7 -    val descr' = List.concat descr;
     8.8 -
     8.9 -    fun make_inj T ((cname, cargs), injs) =
    8.10 -      if null cargs then injs else
    8.11 +    val descr' = flat descr;
    8.12 +    fun make_inj T (cname, cargs) =
    8.13 +      if null cargs then I else
    8.14          let
    8.15            val Ts = map (typ_of_dtyp descr' sorts) cargs;
    8.16            val constr_t = Const (cname, Ts ---> T);
    8.17            val tnames = make_tnames Ts;
    8.18            val frees = map Free (tnames ~~ Ts);
    8.19            val frees' = map Free ((map ((op ^) o (rpair "'")) tnames) ~~ Ts);
    8.20 -        in (HOLogic.mk_Trueprop (HOLogic.mk_eq
    8.21 +        in cons (HOLogic.mk_Trueprop (HOLogic.mk_eq
    8.22            (HOLogic.mk_eq (list_comb (constr_t, frees), list_comb (constr_t, frees')),
    8.23             foldr1 (HOLogic.mk_binop "op &")
    8.24 -             (map HOLogic.mk_eq (frees ~~ frees')))))::injs
    8.25 +             (map HOLogic.mk_eq (frees ~~ frees')))))
    8.26          end;
    8.27 -
    8.28 -  in map (fn (d, T) => foldr (make_inj T) [] (#3 (snd d)))
    8.29 -    ((hd descr) ~~ Library.take (length (hd descr), get_rec_types descr' sorts))
    8.30 +  in
    8.31 +    map2 (fn d => fn T => fold_rev (make_inj T) (#3 (snd d)) [])
    8.32 +      (hd descr) (Library.take (length (hd descr), get_rec_types descr' sorts))
    8.33    end;
    8.34  
    8.35  (********************************* induction **********************************)
     9.1 --- a/src/HOL/Tools/recdef_package.ML	Fri Oct 20 17:07:25 2006 +0200
     9.2 +++ b/src/HOL/Tools/recdef_package.ML	Fri Oct 20 17:07:26 2006 +0200
     9.3 @@ -80,8 +80,6 @@
     9.4      val (del, rest) = List.partition (Library.equal c o fst) congs;
     9.5    in if null del then (warning ("No recdef congruence rule for " ^ quote c); congs) else rest end;
     9.6  
     9.7 -val add_congs = foldr (uncurry add_cong);
     9.8 -
     9.9  end;
    9.10  
    9.11  
    10.1 --- a/src/HOL/Tools/record_package.ML	Fri Oct 20 17:07:25 2006 +0200
    10.2 +++ b/src/HOL/Tools/record_package.ML	Fri Oct 20 17:07:26 2006 +0200
    10.3 @@ -491,7 +491,7 @@
    10.4  
    10.5  
    10.6  fun record_update_tr [t, u] =
    10.7 -      foldr (op $) t (rev (gen_fields_tr "_updates" "_update" updateN u))
    10.8 +      Library.foldr (op $) (rev (gen_fields_tr "_updates" "_update" updateN u), t)
    10.9    | record_update_tr ts = raise TERM ("record_update_tr", ts);
   10.10  
   10.11  fun update_name_tr (Free (x, T) :: ts) = Free (suffix updateN x, T) $$ ts
   10.12 @@ -1547,8 +1547,8 @@
   10.13  (* mk_recordT builds up the record type from the current extension tpye extT and a list
   10.14   * of parent extensions, starting with the root of the record hierarchy
   10.15  *)
   10.16 -fun mk_recordT extT parent_exts =
   10.17 -    foldr (fn ((parent,Ts),T) => Type (parent, subst_last T Ts)) extT parent_exts;
   10.18 +fun mk_recordT extT =
   10.19 +    fold_rev (fn (parent, Ts) => fn T => Type (parent, subst_last T Ts)) extT;
   10.20  
   10.21  
   10.22  
   10.23 @@ -1646,12 +1646,12 @@
   10.24      val extension_id = Library.foldl (op ^) ("",extension_names);
   10.25  
   10.26  
   10.27 -    fun rec_schemeT n = mk_recordT extT (map #extension (prune n parents));
   10.28 +    fun rec_schemeT n = mk_recordT (map #extension (prune n parents)) extT;
   10.29      val rec_schemeT0 = rec_schemeT 0;
   10.30  
   10.31      fun recT n =
   10.32        let val (c,Ts) = extension
   10.33 -      in mk_recordT (Type (c,subst_last HOLogic.unitT Ts))(map #extension (prune n parents))
   10.34 +      in mk_recordT (map #extension (prune n parents)) (Type (c,subst_last HOLogic.unitT Ts))
   10.35        end;
   10.36      val recT0 = recT 0;
   10.37  
    11.1 --- a/src/HOL/Tools/refute.ML	Fri Oct 20 17:07:25 2006 +0200
    11.2 +++ b/src/HOL/Tools/refute.ML	Fri Oct 20 17:07:26 2006 +0200
    11.3 @@ -421,8 +421,8 @@
    11.4  		(* (string * Term.term) list *)
    11.5  		val axioms = Theory.all_axioms_of thy;
    11.6  		(* string list *)
    11.7 -		val rec_names = Symtab.fold (fn (_, info) => fn acc =>
    11.8 -			#rec_names info @ acc) (DatatypePackage.get_datatypes thy) []
    11.9 +		val rec_names = Symtab.fold (append o #rec_names o snd)
   11.10 +          (DatatypePackage.get_datatypes thy) [];
   11.11  		(* string list *)
   11.12  		val const_of_class_names = map Logic.const_of_class (Sign.classes thy)
   11.13  		(* given a constant 's' of type 'T', which is a subterm of 't', where  *)
   11.14 @@ -677,7 +677,7 @@
   11.15  					fun is_IDT_recursor () =
   11.16  						(* I'm not quite sure if checking the name 's' is sufficient, *)
   11.17  						(* or if we should also check the type 'T'                    *)
   11.18 -						s mem rec_names
   11.19 +						member (op =) rec_names s
   11.20  				in
   11.21  					if is_const_of_class () then
   11.22  						(* axiomatic type classes: add "OFCLASS(?'a::c, c_class)" and *)
    12.1 --- a/src/HOL/ex/reflection.ML	Fri Oct 20 17:07:25 2006 +0200
    12.2 +++ b/src/HOL/ex/reflection.ML	Fri Oct 20 17:07:26 2006 +0200
    12.3 @@ -184,8 +184,8 @@
    12.4         val tml = Vartab.dest tmenv
    12.5         val SOME (_,t') = AList.lookup (op =) tml (xn,0)
    12.6         val cvs = 
    12.7 -	   cert (foldr (fn (x,xs) => Const("List.list.Cons", ntT --> ntlT --> ntlT)$x$xs) 
    12.8 -		       (Free(vsn,ntlT)) bsT)
    12.9 +	   cert (fold_rev (fn x => fn xs => Const("List.list.Cons", ntT --> ntlT --> ntlT)$x$xs)
   12.10 +		       bsT (Free (vsn, ntlT)))
   12.11         val cts = map (fn ((vn,vi),(tT,t)) => (cert(Var ((vn,vi),tT)), cert t)) 
   12.12  		     (AList.delete (op =) (xn,0) tml)
   12.13         val th = (instantiate 
   12.14 @@ -232,12 +232,12 @@
   12.15  
   12.16  fun mk_congs ctxt raw_eqs = 
   12.17   let 
   12.18 -  val fs = foldr (fn (eq,fns) => 
   12.19 +  val fs = fold_rev (fn eq =>
   12.20  		     insert (op =) (eq |> prop_of |> HOLogic.dest_Trueprop 
   12.21  			 |> HOLogic.dest_eq |> fst |> strip_comb 
   12.22 -			 |> fst) fns) [] raw_eqs
   12.23 -  val tys = foldr (fn (f,ts) => (f |> fastype_of |> binder_types |> split_last |> fst) 
   12.24 -				    union ts) [] fs
   12.25 +			 |> fst)) raw_eqs []
   12.26 +  val tys = fold_rev (fn f => fn ts => (f |> fastype_of |> binder_types |> split_last |> fst) 
   12.27 +				    union ts) fs []
   12.28    val _ = bds := AList.make (fn _ => ([],[])) tys
   12.29    val (vs, ctxt') = Variable.variant_fixes (replicate (length tys) "vs") ctxt
   12.30    val thy = ProofContext.theory_of ctxt'
    13.1 --- a/src/HOL/ex/svc_funcs.ML	Fri Oct 20 17:07:25 2006 +0200
    13.2 +++ b/src/HOL/ex/svc_funcs.ML	Fri Oct 20 17:07:26 2006 +0200
    13.3 @@ -119,7 +119,7 @@
    13.4     in #1 o tag end;
    13.5  
    13.6   (*Map expression e to 0<=a --> e, where "a" is the name of a nat variable*)
    13.7 - fun add_nat_var (a, e) =
    13.8 + fun add_nat_var a e =
    13.9       Buildin("=>", [Buildin("<=", [Int 0, UnInterp (a, [])]),
   13.10                      e]);
   13.11  
   13.12 @@ -240,7 +240,7 @@
   13.13  
   13.14        val body_e = mt pos body  (*evaluate now to assign into !nat_vars*)
   13.15    in
   13.16 -     foldr add_nat_var body_e (!nat_vars)
   13.17 +     fold_rev add_nat_var (!nat_vars) body_e
   13.18    end;
   13.19  
   13.20  
    14.1 --- a/src/HOL/hologic.ML	Fri Oct 20 17:07:25 2006 +0200
    14.2 +++ b/src/HOL/hologic.ML	Fri Oct 20 17:07:26 2006 +0200
    14.3 @@ -165,7 +165,7 @@
    14.4  
    14.5  fun all_const T = Const ("All", [T --> boolT] ---> boolT);
    14.6  fun mk_all (x, T, P) = all_const T $ absfree (x, T, P);
    14.7 -fun list_all (vs,x) = foldr (fn ((x, T), P) => all_const T $ Abs (x, T, P)) x vs;
    14.8 +fun list_all (vs,x) = Library.foldr (fn ((x, T), P) => all_const T $ Abs (x, T, P)) (vs, x);
    14.9  
   14.10  fun exists_const T = Const ("Ex", [T --> boolT] ---> boolT);
   14.11  fun mk_exists (x, T, P) = exists_const T $ absfree (x, T, P);