--- 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
--- 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
--- 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