# HG changeset patch
# User blanchet
# Date 1328144117 -3600
# Node ID 69f2d19f7d332d122e9b32d3c1b4663d82f1cc99
# Parent  676a4b4b6e736243b2580c61c8cf77c1eddbe722
tuning

diff -r 676a4b4b6e73 -r 69f2d19f7d33 src/HOL/Tools/ATP/atp_problem.ML
--- a/src/HOL/Tools/ATP/atp_problem.ML	Thu Feb 02 01:20:28 2012 +0100
+++ b/src/HOL/Tools/ATP/atp_problem.ML	Thu Feb 02 01:55:17 2012 +0100
@@ -49,7 +49,7 @@
   val introN : string
   val elimN : string
   val simpN : string
-  val eqN : string
+  val spec_eqN : string
   val tptp_cnf : string
   val tptp_fof : string
   val tptp_tff : string
@@ -169,7 +169,7 @@
 val introN = "intro"
 val elimN = "elim"
 val simpN = "simp"
-val eqN = "eq"
+val spec_eqN = "spec_eq"
 
 fun extract_isabelle_info (SOME (ATerm ("[]", [ATerm (s, [])]))) =
     try (unprefix isabelle_info_prefix) s
@@ -441,7 +441,7 @@
       if top_level then
         case extract_isabelle_info info of
           SOME s' => if s' = simpN then s ^ ":lr"
-                     else if s' = eqN then s ^ ":lt"
+                     else if s' = spec_eqN then s ^ ":lt"
                      else s
         | NONE => s
       else
diff -r 676a4b4b6e73 -r 69f2d19f7d33 src/HOL/Tools/ATP/atp_problem_generate.ML
--- a/src/HOL/Tools/ATP/atp_problem_generate.ML	Thu Feb 02 01:20:28 2012 +0100
+++ b/src/HOL/Tools/ATP/atp_problem_generate.ML	Thu Feb 02 01:55:17 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 | Eq
+  datatype status = General | Induct | Intro | Elim | Simp | Spec_Eq
   type stature = scope * status
 
   datatype polymorphism = Polymorphic | Raw_Monomorphic | Mangled_Monomorphic
@@ -549,7 +549,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 | Eq
+datatype status = General | Induct | Intro | Elim | Simp | Spec_Eq
 type stature = scope * status
 
 datatype order = First_Order | Higher_Order
@@ -1207,7 +1207,8 @@
             |>> map2 (fn (name, (kind, _)) => fn t => (name, (kind, t))) facts
     val lam_facts =
       map2 (fn t => fn j =>
-               ((lam_fact_prefix ^ Int.toString j, (Global, Eq)), (Axiom, t)))
+               ((lam_fact_prefix ^ Int.toString j, (Global, Spec_Eq)),
+                (Axiom, t)))
            lambda_ts (1 upto length lambda_ts)
   in (facts, lam_facts) end
 
@@ -1631,7 +1632,7 @@
   in
     Formula (type_tag_idempotence_helper_name, Axiom,
              eq_formula type_enc [] [] false (tag tagged_var) tagged_var,
-             NONE, isabelle_info format eqN)
+             NONE, isabelle_info format spec_eqN)
   end
 
 fun should_specialize_helper type_enc t =
@@ -1659,7 +1660,8 @@
             [t]
         end
         |> tag_list 1
-        |> map (fn (k, t) => ((dub needs_fairly_sound j k, (Global, Eq)), t))
+        |> map (fn (k, t) =>
+                   ((dub needs_fairly_sound j k, (Global, Spec_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
@@ -1955,7 +1957,7 @@
      Intro => isabelle_info format introN
    | Elim => isabelle_info format elimN
    | Simp => isabelle_info format simpN
-   | Eq => isabelle_info format eqN
+   | Spec_Eq => isabelle_info format spec_eqN
    | _ => NONE)
   |> Formula
 
@@ -2200,7 +2202,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,
-             NONE, isabelle_info format eqN)
+             NONE, isabelle_info format spec_eqN)
   end
 
 fun problem_lines_for_mono_types ctxt format mono type_enc Ts =
@@ -2305,7 +2307,7 @@
         in
           cons (Formula (ident_base ^ "_res", kind,
                          eq (tag_with res_T (cst bounds)) (cst tagged_bounds),
-                         NONE, isabelle_info format eqN))
+                         NONE, isabelle_info format spec_eqN))
         end
       else
         I
@@ -2317,7 +2319,7 @@
             cons (Formula (ident_base ^ "_arg" ^ string_of_int (k + 1), kind,
                            eq (cst (bounds1 @ tag_with arg_T bound :: bounds2))
                               (cst bounds),
-                           NONE, isabelle_info format eqN))
+                           NONE, isabelle_info format spec_eqN))
           | _ => raise Fail "expected nonempty tail"
         else
           I
@@ -2422,7 +2424,7 @@
       in
         ([tm1, tm2],
          [Formula (app_op_alias_eq_prefix ^ s2, kind, eq |> maybe_negate, NONE,
-                   isabelle_info format eqN)])
+                   isabelle_info format spec_eqN)])
         |> (if ary - 1 = base_ary orelse Symtab.defined sym_tab s1 then I
             else pair_append (do_alias (ary - 1)))
       end
diff -r 676a4b4b6e73 -r 69f2d19f7d33 src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML	Thu Feb 02 01:20:28 2012 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML	Thu Feb 02 01:55:17 2012 +0100
@@ -128,14 +128,14 @@
       Item_Net.content safeEs @ Item_Net.content hazEs
       |> map Classical.classical_rule
     val simps = ctxt |> simpset_of |> dest_ss |> #simps
-    val eqs =
+    val spec_eqs =
       ctxt |> Spec_Rules.get
            |> filter (curry (op =) Spec_Rules.Equational o fst)
            |> maps (snd o snd)
   in
     Termtab.empty |> add Simp I snd simps
                   |> add Simp atomize snd simps
-                  |> add Eq I I eqs
+                  |> add Spec_Eq I I spec_eqs
                   |> add Elim I I elims
                   |> add Intro I I intros
   end