src/HOL/Import/shuffler.ML
changeset 15570 8d8c70b41bab
parent 15531 08c8dad8e399
child 15574 b1d1b5bfc464
     1.1 --- a/src/HOL/Import/shuffler.ML	Thu Mar 03 09:22:35 2005 +0100
     1.2 +++ b/src/HOL/Import/shuffler.ML	Thu Mar 03 12:43:01 2005 +0100
     1.3 @@ -42,17 +42,17 @@
     1.4    case e of
     1.5       THM (msg,i,thms) =>
     1.6  	 (writeln ("Exception THM " ^ string_of_int i ^ " raised:\n" ^ msg);
     1.7 -	  seq print_thm thms)
     1.8 +	  List.app print_thm thms)
     1.9     | THEORY (msg,thys) =>
    1.10  	 (writeln ("Exception THEORY raised:\n" ^ msg);
    1.11 -	  seq (Pretty.writeln o Display.pretty_theory) thys)
    1.12 +	  List.app (Pretty.writeln o Display.pretty_theory) thys)
    1.13     | TERM (msg,ts) =>
    1.14  	 (writeln ("Exception TERM raised:\n" ^ msg);
    1.15 -	  seq (writeln o Sign.string_of_term sign) ts)
    1.16 +	  List.app (writeln o Sign.string_of_term sign) ts)
    1.17     | TYPE (msg,Ts,ts) =>
    1.18  	 (writeln ("Exception TYPE raised:\n" ^ msg);
    1.19 -	  seq (writeln o Sign.string_of_typ sign) Ts;
    1.20 -	  seq (writeln o Sign.string_of_term sign) ts)
    1.21 +	  List.app (writeln o Sign.string_of_typ sign) Ts;
    1.22 +	  List.app (writeln o Sign.string_of_term sign) ts)
    1.23     | e => raise e
    1.24  
    1.25  (*Prints an exception, then fails*)
    1.26 @@ -251,7 +251,7 @@
    1.27  	val tvars = term_tvars t
    1.28  	val tfree_names = add_term_tfree_names(t,[])
    1.29  	val (type_inst,_) =
    1.30 -	    foldl (fn ((inst,used),(w as (v,_),S)) =>
    1.31 +	    Library.foldl (fn ((inst,used),(w as (v,_),S)) =>
    1.32  		      let
    1.33  			  val v' = variant used v
    1.34  		      in
    1.35 @@ -553,13 +553,13 @@
    1.36      end
    1.37      
    1.38  val collect_ignored =
    1.39 -    foldr (fn (thm,cs) =>
    1.40 +    Library.foldr (fn (thm,cs) =>
    1.41  	      let
    1.42  		  val (lhs,rhs) = Logic.dest_equals (prop_of thm)
    1.43  		  val ignore_lhs = term_consts lhs \\ term_consts rhs
    1.44  		  val ignore_rhs = term_consts rhs \\ term_consts lhs
    1.45  	      in
    1.46 -		  foldr (op ins_string) (ignore_lhs @ ignore_rhs,cs)
    1.47 +		  Library.foldr (op ins_string) (ignore_lhs @ ignore_rhs,cs)
    1.48  	      end)
    1.49  
    1.50  (* set_prop t thms tries to make a theorem with the proposition t from
    1.51 @@ -570,7 +570,7 @@
    1.52      let
    1.53  	val sg = sign_of thy
    1.54  	val vars = add_term_frees (t,add_term_vars (t,[]))
    1.55 -	val closed_t = foldr (fn (v,body) => let val vT = type_of v
    1.56 +	val closed_t = Library.foldr (fn (v,body) => let val vT = type_of v
    1.57  					     in all vT $ (Abs("x",vT,abstract_over(v,body))) end) (vars,t)
    1.58  	val rew_th = norm_term thy closed_t
    1.59  	val rhs = snd (dest_equals (cprop_of rew_th))
    1.60 @@ -614,13 +614,13 @@
    1.61  	val rel_consts = term_consts t \\ ignored
    1.62  	val pot_thms = PureThy.thms_containing_consts thy rel_consts
    1.63      in
    1.64 -	filter (match_consts ignored t) pot_thms
    1.65 +	List.filter (match_consts ignored t) pot_thms
    1.66      end
    1.67  
    1.68  fun gen_shuffle_tac thy search thms i st =
    1.69      let
    1.70  	val _ = message ("Shuffling " ^ (string_of_thm st))
    1.71 -	val t = nth_elem(i-1,prems_of st)
    1.72 +	val t = List.nth(prems_of st,i-1)
    1.73  	val set = set_prop thy t
    1.74  	fun process_tac thms st =
    1.75  	    case set thms of