1.1 --- a/src/HOL/Import/proof_kernel.ML	Tue Oct 20 16:13:01 2009 +0200
     1.2 +++ b/src/HOL/Import/proof_kernel.ML	Wed Oct 21 08:14:38 2009 +0200
     1.3 @@ -1230,7 +1230,7 @@
     1.4            | add_consts (_, cs) = cs
     1.5          val t_consts = add_consts(t,[])
     1.6      in
     1.7 -        fn th => gen_eq_set (op =) (t_consts, add_consts (prop_of th, []))
     1.8 +        fn th => eq_set (op =) (t_consts, add_consts (prop_of th, []))
     1.9      end
    1.10  
    1.11  fun split_name str =