src/HOL/Import/shuffler.ML
changeset 20854 f9cf9e62d11c
parent 20326 cbf31171c147
child 20897 3f8d2834b2c4
     1.1 --- a/src/HOL/Import/shuffler.ML	Wed Oct 04 14:14:33 2006 +0200
     1.2 +++ b/src/HOL/Import/shuffler.ML	Wed Oct 04 14:17:38 2006 +0200
     1.3 @@ -554,7 +554,7 @@
     1.4  	fun add_consts (Const (c, _), cs) =
     1.5  	    if c mem_string ignore
     1.6  	    then cs
     1.7 -	    else c ins_string cs
     1.8 +	    else insert (op =) c cs
     1.9  	  | add_consts (t $ u, cs) = add_consts (t, add_consts (u, cs))
    1.10  	  | add_consts (Abs (_, _, t), cs) = add_consts (t, cs)
    1.11  	  | add_consts (_, cs) = cs
    1.12 @@ -575,7 +575,7 @@
    1.13  		  val ignore_lhs = term_consts lhs \\ term_consts rhs
    1.14  		  val ignore_rhs = term_consts rhs \\ term_consts lhs
    1.15  	      in
    1.16 -		  foldr (op ins_string) cs (ignore_lhs @ ignore_rhs)
    1.17 +		  fold_rev (insert (op =)) cs (ignore_lhs @ ignore_rhs)
    1.18  	      end)
    1.19  
    1.20  (* set_prop t thms tries to make a theorem with the proposition t from