# HG changeset patch
# User blanchet
# Date 1315396217 -7200
# Node ID 3634c6dba23f7bdfb80f6da9d8365431066f879e
# Parent  ba4c0205267f96280f95f7fd06905298417fca69
tuning

diff -r ba4c0205267f -r 3634c6dba23f 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
diff -r ba4c0205267f -r 3634c6dba23f src/HOL/Tools/ATP/atp_translate.ML
--- a/src/HOL/Tools/ATP/atp_translate.ML	Wed Sep 07 13:50:16 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_translate.ML	Wed Sep 07 13:50:17 2011 +0200
@@ -16,8 +16,7 @@
   type 'a problem = 'a ATP_Problem.problem
 
   datatype locality =
-    General | Helper | Induction | Extensionality | Intro | Elim | Simp |
-    Local | Assum | Chained
+    General | Helper | Induction | Intro | Elim | Simp | Local | Assum | Chained
 
   datatype polymorphism = Polymorphic | Raw_Monomorphic | Mangled_Monomorphic
   datatype soundness = Sound_Modulo_Infiniteness | Sound
@@ -526,8 +525,7 @@
     in (IAbs ((name, T), tm), union (op =) atomic_Ts (atyps_of T)) end
 
 datatype locality =
-  General | Helper | Induction | Extensionality | Intro | Elim | Simp |
-  Local | Assum | Chained
+  General | Helper | Induction | Intro | Elim | Simp | Local | Assum | Chained
 
 datatype order = First_Order | Higher_Order
 datatype polymorphism = Polymorphic | Raw_Monomorphic | Mangled_Monomorphic
diff -r ba4c0205267f -r 3634c6dba23f src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML	Wed Sep 07 13:50:16 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML	Wed Sep 07 13:50:17 2011 +0200
@@ -144,7 +144,6 @@
                  (j + 1,
                   ((nth_name j,
                     if member Thm.eq_thm_prop chained_ths th then Chained
-                    else if Thm.eq_thm_prop (th, @{thm ext}) then Extensionality
                     else General), th) :: rest))
     |> snd
   end
@@ -845,8 +844,7 @@
       else if global then
         case Termtab.lookup clasimpset_table (prop_of th) of
           SOME loc => loc
-        | NONE => if Thm.eq_thm_prop (th, @{thm ext}) then Extensionality
-                  else General
+        | NONE => General
       else if is_assum th then Assum else Local
     fun is_good_unnamed_local th =
       not (Thm.has_name_hint th) andalso