src/HOL/Import/shuffler.ML
 changeset 15574 b1d1b5bfc464 parent 15570 8d8c70b41bab child 15661 9ef583b08647
```     1.1 --- a/src/HOL/Import/shuffler.ML	Fri Mar 04 11:44:26 2005 +0100
1.2 +++ b/src/HOL/Import/shuffler.ML	Fri Mar 04 15:07:34 2005 +0100
1.3 @@ -553,13 +553,13 @@
1.4      end
1.5
1.6  val collect_ignored =
1.7 -    Library.foldr (fn (thm,cs) =>
1.8 +    foldr (fn (thm,cs) =>
1.9  	      let
1.10  		  val (lhs,rhs) = Logic.dest_equals (prop_of thm)
1.11  		  val ignore_lhs = term_consts lhs \\ term_consts rhs
1.12  		  val ignore_rhs = term_consts rhs \\ term_consts lhs
1.13  	      in
1.14 -		  Library.foldr (op ins_string) (ignore_lhs @ ignore_rhs,cs)
1.15 +		  foldr (op ins_string) cs (ignore_lhs @ ignore_rhs)
1.16  	      end)
1.17
1.18  (* set_prop t thms tries to make a theorem with the proposition t from
1.19 @@ -570,8 +570,8 @@
1.20      let
1.21  	val sg = sign_of thy
1.23 -	val closed_t = Library.foldr (fn (v,body) => let val vT = type_of v
1.24 -					     in all vT \$ (Abs("x",vT,abstract_over(v,body))) end) (vars,t)
1.25 +	val closed_t = foldr (fn (v,body) => let val vT = type_of v
1.26 +					     in all vT \$ (Abs("x",vT,abstract_over(v,body))) end) t vars
1.27  	val rew_th = norm_term thy closed_t
1.28  	val rhs = snd (dest_equals (cprop_of rew_th))
1.29
1.30 @@ -610,7 +610,7 @@
1.31  fun find_potential thy t =
1.32      let
1.33  	val shuffles = ShuffleData.get thy
1.34 -	val ignored = collect_ignored(shuffles,[])
1.35 +	val ignored = collect_ignored [] shuffles
1.36  	val rel_consts = term_consts t \\ ignored
1.37  	val pot_thms = PureThy.thms_containing_consts thy rel_consts
1.38      in
```