src/HOL/Tools/ATP/atp_reconstruct.ML

--- a/src/HOL/Tools/ATP/atp_reconstruct.ML	Wed Sep 07 13:50:16 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_reconstruct.ML	Wed Sep 07 13:50:17 2011 +0200
@@ -152,7 +152,7 @@
     union (op =) (resolve_fact facts_offset fact_names name)
   | add_fact ctxt _ _ (Inference (_, _, deps)) =
     if AList.defined (op =) deps leo2_ext then
-      insert (op =) (ext_name ctxt, Extensionality)
+      insert (op =) (ext_name ctxt, General)
     else
       I
   | add_fact _ _ _ _ = I