src/HOL/Import/shuffler.ML
changeset 33037 b22e44496dc2
parent 32957 675c0c7e6a37
child 33038 8f9594c31de4
     1.1 --- a/src/HOL/Import/shuffler.ML	Tue Oct 20 13:37:56 2009 +0200
     1.2 +++ b/src/HOL/Import/shuffler.ML	Tue Oct 20 16:13:01 2009 +0200
     1.3 @@ -563,7 +563,7 @@
     1.4          let
     1.5              val th_consts = add_consts(prop_of th,[])
     1.6          in
     1.7 -            eq_set(t_consts,th_consts)
     1.8 +            gen_eq_set (op =) (t_consts, th_consts)
     1.9          end
    1.10      end
    1.11