src/HOL/Import/proof_kernel.ML

           | add_consts (t $ u, cs) = add_consts (t, add_consts (u, cs))
           | add_consts (Abs (_, _, t), cs) = add_consts (t, cs)
           | add_consts (_, cs) = cs
         val t_consts = add_consts(t,[])
     in
-        fn th => gen_eq_set (op =) (t_consts, add_consts (prop_of th, []))
+        fn th => eq_set (op =) (t_consts, add_consts (prop_of th, []))
     end
 
 fun split_name str =
     let
         val sub = Substring.full str