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.22  	val vars = add_term_frees (t,add_term_vars (t,[]))
    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