# HG changeset patch
# User blanchet
# Date 1327607394 -3600
# Node ID ab9d96cc7a991493a4a7cd27606362c5542f3156
# Parent  cac402c486b029ed2bb415011a5da7091f698281
even more lr tags for SPASS -- anything that is considered an "equational rule spec" is relevant

diff -r cac402c486b0 -r ab9d96cc7a99 src/HOL/Tools/ATP/atp_problem_generate.ML
--- a/src/HOL/Tools/ATP/atp_problem_generate.ML	Thu Jan 26 20:49:54 2012 +0100
+++ b/src/HOL/Tools/ATP/atp_problem_generate.ML	Thu Jan 26 20:49:54 2012 +0100
@@ -16,7 +16,7 @@
   type 'a problem = 'a ATP_Problem.problem
 
   datatype scope = Global | Local | Assum | Chained
-  datatype status = General | Induct | Intro | Elim | Simp
+  datatype status = General | Induct | Intro | Elim | Simp | Eq
   type stature = scope * status
 
   datatype polymorphism = Polymorphic | Raw_Monomorphic | Mangled_Monomorphic
@@ -543,7 +543,7 @@
     in (IAbs ((name, T), tm), union (op =) atomic_Ts (atomic_types_of T)) end
 
 datatype scope = Global | Local | Assum | Chained
-datatype status = General | Induct | Intro | Elim | Simp
+datatype status = General | Induct | Intro | Elim | Simp | Eq
 type stature = scope * status
 
 datatype order = First_Order | Higher_Order
@@ -1622,7 +1622,7 @@
             [t]
         end
         |> tag_list 1
-        |> map (fn (k, t) => ((dub needs_fairly_sound j k, (Global, Simp)), t))
+        |> map (fn (k, t) => ((dub needs_fairly_sound j k, (Global, Eq)), t))
       val make_facts = map_filter (make_fact ctxt format type_enc false)
       val fairly_sound = is_type_enc_fairly_sound type_enc
     in
@@ -1909,6 +1909,7 @@
      Intro => isabelle_info format introN
    | Elim => isabelle_info format elimN
    | Simp => isabelle_info format simpN
+   | Eq => isabelle_info format simpN
    | _ => NONE)
   |> Formula
 
diff -r cac402c486b0 -r ab9d96cc7a99 src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML	Thu Jan 26 20:49:54 2012 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML	Thu Jan 26 20:49:54 2012 +0100
@@ -793,11 +793,16 @@
       Item_Net.content safeEs @ Item_Net.content hazEs
       |> map Classical.classical_rule
     val simps = ctxt |> simpset_of |> dest_ss |> #simps
+    val eqs =
+      ctxt |> Spec_Rules.get
+           |> filter (curry (op =) Spec_Rules.Equational o fst)
+           |> maps (snd o snd)
   in
-    Termtab.empty |> add Intro I I intros
-                  |> add Elim I I elims
+    Termtab.empty |> add Eq I I eqs
                   |> add Simp I snd simps
                   |> add Simp atomize snd simps
+                  |> add Elim I I elims
+                  |> add Intro I I intros
   end
 
 fun all_facts ctxt ho_atp reserved exporter add_ths chained_ths =