diff -r 7769bf5c2a17 -r de5dd84717c1 src/HOL/Tools/ATP/atp_problem_generate.ML
--- a/src/HOL/Tools/ATP/atp_problem_generate.ML	Tue Jan 31 10:29:05 2012 +0100
+++ b/src/HOL/Tools/ATP/atp_problem_generate.ML	Tue Jan 31 12:43:48 2012 +0100
@@ -1600,7 +1600,7 @@
   in
     Formula (type_tag_idempotence_helper_name, Axiom,
              eq_formula type_enc [] false (tag tagged_var) tagged_var,
-             isabelle_info format simpN, NONE)
+             isabelle_info format eqN, NONE)
   end
 
 fun should_specialize_helper type_enc t =
@@ -1921,7 +1921,7 @@
      Intro => isabelle_info format introN
    | Elim => isabelle_info format elimN
    | Simp => isabelle_info format simpN
-   | Eq => isabelle_info format simpN
+   | Eq => isabelle_info format eqN
    | _ => NONE)
   |> Formula
 
@@ -2164,7 +2164,7 @@
              Axiom,
              eq_formula type_enc (atomic_types_of T) false
                   (tag_with_type ctxt format mono type_enc NONE T x_var) x_var,
-             isabelle_info format simpN, NONE)
+             isabelle_info format eqN, NONE)
   end
 
 fun problem_lines_for_mono_types ctxt format mono type_enc Ts =
@@ -2269,7 +2269,7 @@
         in
           cons (Formula (ident_base ^ "_res", kind,
                          eq (tag_with res_T (cst bounds)) (cst tagged_bounds),
-                         isabelle_info format simpN, NONE))
+                         isabelle_info format eqN, NONE))
         end
       else
         I
@@ -2281,7 +2281,7 @@
             cons (Formula (ident_base ^ "_arg" ^ string_of_int (k + 1), kind,
                            eq (cst (bounds1 @ tag_with arg_T bound :: bounds2))
                               (cst bounds),
-                           isabelle_info format simpN, NONE))
+                           isabelle_info format eqN, NONE))
           | _ => raise Fail "expected nonempty tail"
         else
           I