renamed "preds" encodings to "guards"

--- a/src/HOL/Metis_Examples/Proxies.thy	Tue Jul 26 18:11:38 2011 +0200
+++ b/src/HOL/Metis_Examples/Proxies.thy	Tue Jul 26 22:53:06 2011 +0200
@@ -60,60 +60,60 @@
 sledgehammer [type_enc = erased, expect = none] (id_apply)
 sledgehammer [type_enc = poly_tags?, expect = some] (id_apply)
 sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
-sledgehammer [type_enc = poly_preds?, expect = some] (id_apply)
-sledgehammer [type_enc = poly_preds, expect = some] (id_apply)
+sledgehammer [type_enc = poly_guards?, expect = some] (id_apply)
+sledgehammer [type_enc = poly_guards, expect = some] (id_apply)
 sledgehammer [type_enc = mangled_tags?, expect = some] (id_apply)
 sledgehammer [type_enc = mangled_tags, expect = some] (id_apply)
-sledgehammer [type_enc = mangled_preds?, expect = some] (id_apply)
-sledgehammer [type_enc = mangled_preds, expect = some] (id_apply)
+sledgehammer [type_enc = mangled_guards?, expect = some] (id_apply)
+sledgehammer [type_enc = mangled_guards, expect = some] (id_apply)
 by (metis (full_types) id_apply)
 
 lemma "id True"
 sledgehammer [type_enc = erased, expect = some] (id_apply)
 sledgehammer [type_enc = poly_tags?, expect = some] (id_apply)
 sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
-sledgehammer [type_enc = poly_preds?, expect = some] (id_apply)
-sledgehammer [type_enc = poly_preds, expect = some] (id_apply)
+sledgehammer [type_enc = poly_guards?, expect = some] (id_apply)
+sledgehammer [type_enc = poly_guards, expect = some] (id_apply)
 sledgehammer [type_enc = mangled_tags?, expect = some] (id_apply)
 sledgehammer [type_enc = mangled_tags, expect = some] (id_apply)
-sledgehammer [type_enc = mangled_preds?, expect = some] (id_apply)
-sledgehammer [type_enc = mangled_preds, expect = some] (id_apply)
+sledgehammer [type_enc = mangled_guards?, expect = some] (id_apply)
+sledgehammer [type_enc = mangled_guards, expect = some] (id_apply)
 by (metis_exhaust id_apply)
 
 lemma "\<not> id False"
 sledgehammer [type_enc = erased, expect = some] (id_apply)
 sledgehammer [type_enc = poly_tags?, expect = some] (id_apply)
 sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
-sledgehammer [type_enc = poly_preds?, expect = some] (id_apply)
-sledgehammer [type_enc = poly_preds, expect = some] (id_apply)
+sledgehammer [type_enc = poly_guards?, expect = some] (id_apply)
+sledgehammer [type_enc = poly_guards, expect = some] (id_apply)
 sledgehammer [type_enc = mangled_tags?, expect = some] (id_apply)
 sledgehammer [type_enc = mangled_tags, expect = some] (id_apply)
-sledgehammer [type_enc = mangled_preds?, expect = some] (id_apply)
-sledgehammer [type_enc = mangled_preds, expect = some] (id_apply)
+sledgehammer [type_enc = mangled_guards?, expect = some] (id_apply)
+sledgehammer [type_enc = mangled_guards, expect = some] (id_apply)
 by (metis_exhaust id_apply)
 
 lemma "x = id True \<or> x = id False"
 sledgehammer [type_enc = erased, expect = some] (id_apply)
 sledgehammer [type_enc = poly_tags?, expect = some] (id_apply)
 sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
-sledgehammer [type_enc = poly_preds?, expect = some] (id_apply)
-sledgehammer [type_enc = poly_preds, expect = some] (id_apply)
+sledgehammer [type_enc = poly_guards?, expect = some] (id_apply)
+sledgehammer [type_enc = poly_guards, expect = some] (id_apply)
 sledgehammer [type_enc = mangled_tags?, expect = some] (id_apply)
 sledgehammer [type_enc = mangled_tags, expect = some] (id_apply)
-sledgehammer [type_enc = mangled_preds?, expect = some] (id_apply)
-sledgehammer [type_enc = mangled_preds, expect = some] (id_apply)
+sledgehammer [type_enc = mangled_guards?, expect = some] (id_apply)
+sledgehammer [type_enc = mangled_guards, expect = some] (id_apply)
 by (metis_exhaust id_apply)
 
 lemma "id x = id True \<or> id x = id False"
 sledgehammer [type_enc = erased, expect = some] (id_apply)
 sledgehammer [type_enc = poly_tags?, expect = some] (id_apply)
 sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
-sledgehammer [type_enc = poly_preds?, expect = some] (id_apply)
-sledgehammer [type_enc = poly_preds, expect = some] (id_apply)
+sledgehammer [type_enc = poly_guards?, expect = some] (id_apply)
+sledgehammer [type_enc = poly_guards, expect = some] (id_apply)
 sledgehammer [type_enc = mangled_tags?, expect = some] (id_apply)
 sledgehammer [type_enc = mangled_tags, expect = some] (id_apply)
-sledgehammer [type_enc = mangled_preds?, expect = some] (id_apply)
-sledgehammer [type_enc = mangled_preds, expect = some] (id_apply)
+sledgehammer [type_enc = mangled_guards?, expect = some] (id_apply)
+sledgehammer [type_enc = mangled_guards, expect = some] (id_apply)
 by (metis_exhaust id_apply)
 
 lemma "P True \<Longrightarrow> P False \<Longrightarrow> P x"
@@ -121,144 +121,144 @@
 sledgehammer [type_enc = poly_args, expect = none] ()
 sledgehammer [type_enc = poly_tags?, expect = some] ()
 sledgehammer [type_enc = poly_tags, expect = some] ()
-sledgehammer [type_enc = poly_preds?, expect = some] (id_apply)
-sledgehammer [type_enc = poly_preds, expect = some] ()
+sledgehammer [type_enc = poly_guards?, expect = some] (id_apply)
+sledgehammer [type_enc = poly_guards, expect = some] ()
 sledgehammer [type_enc = mangled_tags?, expect = some] ()
 sledgehammer [type_enc = mangled_tags, expect = some] ()
-sledgehammer [type_enc = mangled_preds?, expect = some] ()
-sledgehammer [type_enc = mangled_preds, expect = some] ()
+sledgehammer [type_enc = mangled_guards?, expect = some] ()
+sledgehammer [type_enc = mangled_guards, expect = some] ()
 by (metis (full_types))
 
 lemma "id (\<not> a) \<Longrightarrow> \<not> id a"
 sledgehammer [type_enc = erased, expect = some] (id_apply)
 sledgehammer [type_enc = poly_tags?, expect = some] (id_apply)
 sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
-sledgehammer [type_enc = poly_preds?, expect = some] (id_apply)
-sledgehammer [type_enc = poly_preds, expect = some] (id_apply)
+sledgehammer [type_enc = poly_guards?, expect = some] (id_apply)
+sledgehammer [type_enc = poly_guards, expect = some] (id_apply)
 sledgehammer [type_enc = mangled_tags?, expect = some] (id_apply)
 sledgehammer [type_enc = mangled_tags, expect = some] (id_apply)
-sledgehammer [type_enc = mangled_preds?, expect = some] (id_apply)
-sledgehammer [type_enc = mangled_preds, expect = some] (id_apply)
+sledgehammer [type_enc = mangled_guards?, expect = some] (id_apply)
+sledgehammer [type_enc = mangled_guards, expect = some] (id_apply)
 by (metis_exhaust id_apply)
 
 lemma "id (\<not> \<not> a) \<Longrightarrow> id a"
 sledgehammer [type_enc = erased, expect = some] (id_apply)
 sledgehammer [type_enc = poly_tags?, expect = some] (id_apply)
 sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
-sledgehammer [type_enc = poly_preds?, expect = some] (id_apply)
-sledgehammer [type_enc = poly_preds, expect = some] (id_apply)
+sledgehammer [type_enc = poly_guards?, expect = some] (id_apply)
+sledgehammer [type_enc = poly_guards, expect = some] (id_apply)
 sledgehammer [type_enc = mangled_tags?, expect = some] (id_apply)
 sledgehammer [type_enc = mangled_tags, expect = some] (id_apply)
-sledgehammer [type_enc = mangled_preds?, expect = some] (id_apply)
-sledgehammer [type_enc = mangled_preds, expect = some] (id_apply)
+sledgehammer [type_enc = mangled_guards?, expect = some] (id_apply)
+sledgehammer [type_enc = mangled_guards, expect = some] (id_apply)
 by (metis_exhaust id_apply)
 
 lemma "id (\<not> (id (\<not> a))) \<Longrightarrow> id a"
 sledgehammer [type_enc = erased, expect = some] (id_apply)
 sledgehammer [type_enc = poly_tags?, expect = some] (id_apply)
 sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
-sledgehammer [type_enc = poly_preds?, expect = some] (id_apply)
-sledgehammer [type_enc = poly_preds, expect = some] (id_apply)
+sledgehammer [type_enc = poly_guards?, expect = some] (id_apply)
+sledgehammer [type_enc = poly_guards, expect = some] (id_apply)
 sledgehammer [type_enc = mangled_tags?, expect = some] (id_apply)
 sledgehammer [type_enc = mangled_tags, expect = some] (id_apply)
-sledgehammer [type_enc = mangled_preds?, expect = some] (id_apply)
-sledgehammer [type_enc = mangled_preds, expect = some] (id_apply)
+sledgehammer [type_enc = mangled_guards?, expect = some] (id_apply)
+sledgehammer [type_enc = mangled_guards, expect = some] (id_apply)
 by (metis_exhaust id_apply)
 
 lemma "id (a \<and> b) \<Longrightarrow> id a"
 sledgehammer [type_enc = erased, expect = some] (id_apply)
 sledgehammer [type_enc = poly_tags?, expect = some] (id_apply)
 sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
-sledgehammer [type_enc = poly_preds?, expect = some] (id_apply)
-sledgehammer [type_enc = poly_preds, expect = some] (id_apply)
+sledgehammer [type_enc = poly_guards?, expect = some] (id_apply)
+sledgehammer [type_enc = poly_guards, expect = some] (id_apply)
 sledgehammer [type_enc = mangled_tags?, expect = some] (id_apply)
 sledgehammer [type_enc = mangled_tags, expect = some] (id_apply)
-sledgehammer [type_enc = mangled_preds?, expect = some] (id_apply)
-sledgehammer [type_enc = mangled_preds, expect = some] (id_apply)
+sledgehammer [type_enc = mangled_guards?, expect = some] (id_apply)
+sledgehammer [type_enc = mangled_guards, expect = some] (id_apply)
 by (metis_exhaust id_apply)
 
 lemma "id (a \<and> b) \<Longrightarrow> id b"
 sledgehammer [type_enc = erased, expect = some] (id_apply)
 sledgehammer [type_enc = poly_tags?, expect = some] (id_apply)
 sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
-sledgehammer [type_enc = poly_preds?, expect = some] (id_apply)
-sledgehammer [type_enc = poly_preds, expect = some] (id_apply)
+sledgehammer [type_enc = poly_guards?, expect = some] (id_apply)
+sledgehammer [type_enc = poly_guards, expect = some] (id_apply)
 sledgehammer [type_enc = mangled_tags?, expect = some] (id_apply)
 sledgehammer [type_enc = mangled_tags, expect = some] (id_apply)
-sledgehammer [type_enc = mangled_preds?, expect = some] (id_apply)
-sledgehammer [type_enc = mangled_preds, expect = some] (id_apply)
+sledgehammer [type_enc = mangled_guards?, expect = some] (id_apply)
+sledgehammer [type_enc = mangled_guards, expect = some] (id_apply)
 by (metis_exhaust id_apply)
 
 lemma "id a \<Longrightarrow> id b \<Longrightarrow> id (a \<and> b)"
 sledgehammer [type_enc = erased, expect = some] (id_apply)
 sledgehammer [type_enc = poly_tags?, expect = some] (id_apply)
 sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
-sledgehammer [type_enc = poly_preds?, expect = some] (id_apply)
-sledgehammer [type_enc = poly_preds, expect = some] (id_apply)
+sledgehammer [type_enc = poly_guards?, expect = some] (id_apply)
+sledgehammer [type_enc = poly_guards, expect = some] (id_apply)
 sledgehammer [type_enc = mangled_tags?, expect = some] (id_apply)
 sledgehammer [type_enc = mangled_tags, expect = some] (id_apply)
-sledgehammer [type_enc = mangled_preds?, expect = some] (id_apply)
-sledgehammer [type_enc = mangled_preds, expect = some] (id_apply)
+sledgehammer [type_enc = mangled_guards?, expect = some] (id_apply)
+sledgehammer [type_enc = mangled_guards, expect = some] (id_apply)
 by (metis_exhaust id_apply)
 
 lemma "id a \<Longrightarrow> id (a \<or> b)"
 sledgehammer [type_enc = erased, expect = some] (id_apply)
 sledgehammer [type_enc = poly_tags?, expect = some] (id_apply)
 sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
-sledgehammer [type_enc = poly_preds?, expect = some] (id_apply)
-sledgehammer [type_enc = poly_preds, expect = some] (id_apply)
+sledgehammer [type_enc = poly_guards?, expect = some] (id_apply)
+sledgehammer [type_enc = poly_guards, expect = some] (id_apply)
 sledgehammer [type_enc = mangled_tags?, expect = some] (id_apply)
 sledgehammer [type_enc = mangled_tags, expect = some] (id_apply)
-sledgehammer [type_enc = mangled_preds?, expect = some] (id_apply)
-sledgehammer [type_enc = mangled_preds, expect = some] (id_apply)
+sledgehammer [type_enc = mangled_guards?, expect = some] (id_apply)
+sledgehammer [type_enc = mangled_guards, expect = some] (id_apply)
 by (metis_exhaust id_apply)
 
 lemma "id b \<Longrightarrow> id (a \<or> b)"
 sledgehammer [type_enc = erased, expect = some] (id_apply)
 sledgehammer [type_enc = poly_tags?, expect = some] (id_apply)
 sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
-sledgehammer [type_enc = poly_preds?, expect = some] (id_apply)
-sledgehammer [type_enc = poly_preds, expect = some] (id_apply)
+sledgehammer [type_enc = poly_guards?, expect = some] (id_apply)
+sledgehammer [type_enc = poly_guards, expect = some] (id_apply)
 sledgehammer [type_enc = mangled_tags?, expect = some] (id_apply)
 sledgehammer [type_enc = mangled_tags, expect = some] (id_apply)
-sledgehammer [type_enc = mangled_preds?, expect = some] (id_apply)
-sledgehammer [type_enc = mangled_preds, expect = some] (id_apply)
+sledgehammer [type_enc = mangled_guards?, expect = some] (id_apply)
+sledgehammer [type_enc = mangled_guards, expect = some] (id_apply)
 by (metis_exhaust id_apply)
 
 lemma "id (\<not> a) \<Longrightarrow> id (\<not> b) \<Longrightarrow> id (\<not> (a \<or> b))"
 sledgehammer [type_enc = erased, expect = some] (id_apply)
 sledgehammer [type_enc = poly_tags?, expect = some] (id_apply)
 sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
-sledgehammer [type_enc = poly_preds?, expect = some] (id_apply)
-sledgehammer [type_enc = poly_preds, expect = some] (id_apply)
+sledgehammer [type_enc = poly_guards?, expect = some] (id_apply)
+sledgehammer [type_enc = poly_guards, expect = some] (id_apply)
 sledgehammer [type_enc = mangled_tags?, expect = some] (id_apply)
 sledgehammer [type_enc = mangled_tags, expect = some] (id_apply)
-sledgehammer [type_enc = mangled_preds?, expect = some] (id_apply)
-sledgehammer [type_enc = mangled_preds, expect = some] (id_apply)
+sledgehammer [type_enc = mangled_guards?, expect = some] (id_apply)
+sledgehammer [type_enc = mangled_guards, expect = some] (id_apply)
 by (metis_exhaust id_apply)
 
 lemma "id (\<not> a) \<Longrightarrow> id (a \<longrightarrow> b)"
 sledgehammer [type_enc = erased, expect = some] (id_apply)
 sledgehammer [type_enc = poly_tags?, expect = some] (id_apply)
 sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
-sledgehammer [type_enc = poly_preds?, expect = some] (id_apply)
-sledgehammer [type_enc = poly_preds, expect = some] (id_apply)
+sledgehammer [type_enc = poly_guards?, expect = some] (id_apply)
+sledgehammer [type_enc = poly_guards, expect = some] (id_apply)
 sledgehammer [type_enc = mangled_tags?, expect = some] (id_apply)
 sledgehammer [type_enc = mangled_tags, expect = some] (id_apply)
-sledgehammer [type_enc = mangled_preds?, expect = some] (id_apply)
-sledgehammer [type_enc = mangled_preds, expect = some] (id_apply)
+sledgehammer [type_enc = mangled_guards?, expect = some] (id_apply)
+sledgehammer [type_enc = mangled_guards, expect = some] (id_apply)
 by (metis_exhaust id_apply)
 
 lemma "id (a \<longrightarrow> b) \<longleftrightarrow> id (\<not> a \<or> b)"
 sledgehammer [type_enc = erased, expect = some] (id_apply)
 sledgehammer [type_enc = poly_tags?, expect = some] (id_apply)
 sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
-sledgehammer [type_enc = poly_preds?, expect = some] (id_apply)
-sledgehammer [type_enc = poly_preds, expect = some] (id_apply)
+sledgehammer [type_enc = poly_guards?, expect = some] (id_apply)
+sledgehammer [type_enc = poly_guards, expect = some] (id_apply)
 sledgehammer [type_enc = mangled_tags?, expect = some] (id_apply)
 sledgehammer [type_enc = mangled_tags, expect = some] (id_apply)
-sledgehammer [type_enc = mangled_preds?, expect = some] (id_apply)
-sledgehammer [type_enc = mangled_preds, expect = some] (id_apply)
+sledgehammer [type_enc = mangled_guards?, expect = some] (id_apply)
+sledgehammer [type_enc = mangled_guards, expect = some] (id_apply)
 by (metis_exhaust id_apply)
 
 end

--- a/src/HOL/Metis_Examples/Type_Encodings.thy	Tue Jul 26 18:11:38 2011 +0200
+++ b/src/HOL/Metis_Examples/Type_Encodings.thy	Tue Jul 26 22:53:06 2011 +0200
@@ -26,45 +26,45 @@
    tests. *)
 val type_encs =
   ["erased",
-   "poly_preds",
-   "poly_preds_heavy",
+   "poly_guards",
+   "poly_guards_heavy",
    "poly_tags",
    "poly_tags_heavy",
    "poly_args",
-   "mono_preds",
-   "mono_preds_heavy",
+   "mono_guards",
+   "mono_guards_heavy",
    "mono_tags",
    "mono_tags_heavy",
    "mono_args",
-   "mangled_preds",
-   "mangled_preds_heavy",
+   "mangled_guards",
+   "mangled_guards_heavy",
    "mangled_tags",
    "mangled_tags_heavy",
    "mangled_args",
    "simple",
-   "poly_preds?",
-   "poly_preds_heavy?",
+   "poly_guards?",
+   "poly_guards_heavy?",
    "poly_tags?",
 (* "poly_tags_heavy?", *)
-   "mono_preds?",
-   "mono_preds_heavy?",
+   "mono_guards?",
+   "mono_guards_heavy?",
    "mono_tags?",
    "mono_tags_heavy?",
-   "mangled_preds?",
-   "mangled_preds_heavy?",
+   "mangled_guards?",
+   "mangled_guards_heavy?",
    "mangled_tags?",
    "mangled_tags_heavy?",
    "simple?",
-   "poly_preds!",
-   "poly_preds_heavy!",
+   "poly_guards!",
+   "poly_guards_heavy!",
 (* "poly_tags!", *)
    "poly_tags_heavy!",
-   "mono_preds!",
-   "mono_preds_heavy!",
+   "mono_guards!",
+   "mono_guards_heavy!",
    "mono_tags!",
    "mono_tags_heavy!",
-   "mangled_preds!",
-   "mangled_preds_heavy!",
+   "mangled_guards!",
+   "mangled_guards_heavy!",
    "mangled_tags!",
    "mangled_tags_heavy!",
    "simple!"]

--- a/src/HOL/Tools/ATP/atp_systems.ML	Tue Jul 26 18:11:38 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_systems.ML	Tue Jul 26 22:53:06 2011 +0200
@@ -219,7 +219,7 @@
        (* FUDGE *)
        if method = e_smartN then
          [(0.333, (true, (500, "mangled_tags?", e_fun_weightN))),
-          (0.334, (true, (50, "mangled_preds?", e_fun_weightN))),
+          (0.334, (true, (50, "mangled_guards?", e_fun_weightN))),
           (0.333, (true, (1000, "mangled_tags?", e_sym_offset_weightN)))]
        else
          [(1.0, (true, (500, "mangled_tags?", method)))]
@@ -298,8 +298,8 @@
    formats = [FOF],
    best_slices = fn ctxt =>
      (* FUDGE *)
-     [(0.333, (false, (150, "poly_preds", sosN))),
-      (0.334, (true, (50, "mangled_preds?", no_sosN))),
+     [(0.333, (false, (150, "poly_guards", sosN))),
+      (0.334, (true, (50, "mangled_guards?", no_sosN))),
       (0.333, (false, (500, "mangled_tags?", sosN)))]
      |> (if Config.get ctxt vampire_force_sos then hd #> apfst (K 1.0) #> single
          else I)}
@@ -326,10 +326,10 @@
    formats = [FOF],
    best_slices =
      (* FUDGE (FIXME) *)
-     K [(0.5, (false, (250, "mangled_preds?", ""))),
-        (0.25, (false, (125, "mangled_preds?", ""))),
-        (0.125, (false, (62, "mangled_preds?", ""))),
-        (0.125, (false, (31, "mangled_preds?", "")))]}
+     K [(0.5, (false, (250, "mangled_guards?", ""))),
+        (0.25, (false, (125, "mangled_guards?", ""))),
+        (0.125, (false, (62, "mangled_guards?", ""))),
+        (0.125, (false, (31, "mangled_guards?", "")))]}
 
 val z3_atp = (z3_atpN, z3_atp_config)
 
@@ -413,9 +413,9 @@
                (K (750, "mangled_tags?") (* FUDGE *))
 val remote_vampire =
   remotify_atp vampire "Vampire" ["0.6", "9.0", "1.0"]
-               (K (200, "mangled_preds?") (* FUDGE *))
+               (K (200, "mangled_guards?") (* FUDGE *))
 val remote_z3_atp =
-  remotify_atp z3_atp "Z3" ["2.18"] (K (250, "mangled_preds?") (* FUDGE *))
+  remotify_atp z3_atp "Z3" ["2.18"] (K (250, "mangled_guards?") (* FUDGE *))
 val remote_leo2 =
   remote_atp leo2N "LEO-II" ["1.2.6"] [] [] Axiom Hypothesis [THF]
              (K (100, "simple_higher") (* FUDGE *))
@@ -424,7 +424,7 @@
              (K (64, "simple_higher") (* FUDGE *))
 val remote_sine_e =
   remote_atp sine_eN "SInE" ["0.4"] [] (#known_failures e_config) Axiom
-             Conjecture [FOF] (K (500, "mangled_preds?") (* FUDGE *))
+             Conjecture [FOF] (K (500, "mangled_guards?") (* FUDGE *))
 val remote_snark =
   remote_atp snarkN "SNARK" ["20080805r029", "20080805r024"]
              [("refutation.", "end_refutation.")] [] Hypothesis Hypothesis

--- a/src/HOL/Tools/ATP/atp_translate.ML	Tue Jul 26 18:11:38 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_translate.ML	Tue Jul 26 22:53:06 2011 +0200
@@ -28,7 +28,7 @@
 
   datatype type_enc =
     Simple_Types of order * type_level |
-    Preds of polymorphism * type_level * type_heaviness |
+    Guards of polymorphism * type_level * type_heaviness |
     Tags of polymorphism * type_level * type_heaviness
 
   val bound_var_prefix : string
@@ -45,7 +45,7 @@
   val new_skolem_const_prefix : string
   val type_decl_prefix : string
   val sym_decl_prefix : string
-  val preds_sym_formula_prefix : string
+  val guards_sym_formula_prefix : string
   val lightweight_tags_sym_formula_prefix : string
   val fact_prefix : string
   val conjecture_prefix : string
@@ -133,7 +133,7 @@
 
 val type_decl_prefix = "ty_"
 val sym_decl_prefix = "sy_"
-val preds_sym_formula_prefix = "psy_"
+val guards_sym_formula_prefix = "gsy_"
 val lightweight_tags_sym_formula_prefix = "tsy_"
 val fact_prefix = "fact_"
 val conjecture_prefix = "conj_"
@@ -518,7 +518,7 @@
 
 datatype type_enc =
   Simple_Types of order * type_level |
-  Preds of polymorphism * type_level * type_heaviness |
+  Guards of polymorphism * type_level * type_heaviness |
   Tags of polymorphism * type_level * type_heaviness
 
 fun try_unsuffixes ss s =
@@ -554,14 +554,14 @@
          | ("simple_higher", (NONE, _, Lightweight)) =>
            if level = Noninf_Nonmono_Types then raise Same.SAME
            else Simple_Types (Higher_Order, level)
-         | ("preds", (SOME poly, _, _)) => Preds (poly, level, heaviness)
+         | ("guards", (SOME poly, _, _)) => Guards (poly, level, heaviness)
          | ("tags", (SOME Polymorphic, _, _)) =>
            Tags (Polymorphic, level, heaviness)
          | ("tags", (SOME poly, _, _)) => Tags (poly, level, heaviness)
          | ("args", (SOME poly, All_Types (* naja *), Lightweight)) =>
-           Preds (poly, Const_Arg_Types, Lightweight)
+           Guards (poly, Const_Arg_Types, Lightweight)
          | ("erased", (NONE, All_Types (* naja *), Lightweight)) =>
-           Preds (Polymorphic, No_Types, Lightweight)
+           Guards (Polymorphic, No_Types, Lightweight)
          | _ => raise Same.SAME)
   handle Same.SAME => error ("Unknown type system: " ^ quote s ^ ".")
 
@@ -569,15 +569,15 @@
   | is_type_enc_higher_order _ = false
 
 fun polymorphism_of_type_enc (Simple_Types _) = Mangled_Monomorphic
-  | polymorphism_of_type_enc (Preds (poly, _, _)) = poly
+  | polymorphism_of_type_enc (Guards (poly, _, _)) = poly
   | polymorphism_of_type_enc (Tags (poly, _, _)) = poly
 
 fun level_of_type_enc (Simple_Types (_, level)) = level
-  | level_of_type_enc (Preds (_, level, _)) = level
+  | level_of_type_enc (Guards (_, level, _)) = level
   | level_of_type_enc (Tags (_, level, _)) = level
 
 fun heaviness_of_type_enc (Simple_Types _) = Heavyweight
-  | heaviness_of_type_enc (Preds (_, _, heaviness)) = heaviness
+  | heaviness_of_type_enc (Guards (_, _, heaviness)) = heaviness
   | heaviness_of_type_enc (Tags (_, _, heaviness)) = heaviness
 
 fun is_type_level_virtually_sound level =
@@ -595,13 +595,13 @@
     else if member (op =) formats TFF then
       (TFF, Simple_Types (First_Order, level))
     else
-      choose_format formats (Preds (Mangled_Monomorphic, level, Heavyweight))
+      choose_format formats (Guards (Mangled_Monomorphic, level, Heavyweight))
   | choose_format formats type_enc =
     (case hd formats of
        CNF_UEQ =>
        (CNF_UEQ, case type_enc of
-                   Preds stuff =>
-                   (if is_type_enc_fairly_sound type_enc then Tags else Preds)
+                   Guards stuff =>
+                   (if is_type_enc_fairly_sound type_enc then Tags else Guards)
                        stuff
                  | _ => type_enc)
      | format => (format, type_enc))
@@ -1035,7 +1035,7 @@
     is_type_surely_finite ctxt false T
   | should_encode_type _ _ _ _ = false
 
-fun should_predicate_on_type ctxt nonmono_Ts (Preds (_, level, heaviness))
+fun should_predicate_on_type ctxt nonmono_Ts (Guards (_, level, heaviness))
                              should_predicate_on_var T =
     (heaviness = Heavyweight orelse should_predicate_on_var ()) andalso
     should_encode_type ctxt nonmono_Ts level T
@@ -1756,7 +1756,7 @@
           |> ho_type_from_typ format type_enc pred_sym (length T_arg_Ts + ary))
   end
 
-fun formula_line_for_preds_sym_decl ctxt format conj_sym_kind nonmono_Ts
+fun formula_line_for_guards_sym_decl ctxt format conj_sym_kind nonmono_Ts
         poly_nonmono_Ts type_enc n s j (s', T_args, T, _, ary, in_conj) =
   let
     val (kind, maybe_negate) =
@@ -1775,7 +1775,7 @@
     val bound_Ts =
       arg_Ts |> map (fn T => if should_keep_arg_type T then SOME T else NONE)
   in
-    Formula (preds_sym_formula_prefix ^ s ^
+    Formula (guards_sym_formula_prefix ^ s ^
              (if n > 1 then "_" ^ string_of_int j else ""), kind,
              IConst ((s, s'), T, T_args)
              |> fold (curry (IApp o swap)) bounds
@@ -1851,7 +1851,7 @@
   case type_enc of
     Simple_Types _ =>
     decls |> map (decl_line_for_sym ctxt format nonmono_Ts type_enc s)
-  | Preds _ =>
+  | Guards _ =>
     let
       val decls =
         case decls of
@@ -1871,7 +1871,7 @@
                          o result_type_of_decl)
     in
       (0 upto length decls - 1, decls)
-      |-> map2 (formula_line_for_preds_sym_decl ctxt format conj_sym_kind
+      |-> map2 (formula_line_for_guards_sym_decl ctxt format conj_sym_kind
                    nonmono_Ts poly_nonmono_Ts type_enc n s)
     end
   | Tags (_, _, heaviness) =>

--- a/src/HOL/Tools/Metis/metis_tactics.ML	Tue Jul 26 18:11:38 2011 +0200
+++ b/src/HOL/Tools/Metis/metis_tactics.ML	Tue Jul 26 22:53:06 2011 +0200
@@ -40,7 +40,7 @@
 val no_typesN = "no_types"
 
 val really_full_type_enc = "mangled_tags_heavy"
-val full_type_enc = "poly_preds_heavy_query"
+val full_type_enc = "poly_guards_heavy_query"
 val partial_type_enc = "poly_args"
 val no_type_enc = "erased"
 

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Tue Jul 26 18:11:38 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Tue Jul 26 22:53:06 2011 +0200
@@ -148,7 +148,7 @@
                             | _ => value)
     | NONE => (name, value)
 
-(* Ensure that type systems such as "simple!" and "mangled_preds?" are handled
+(* Ensure that type systems such as "simple!" and "mangled_guards?" are handled
    correctly. *)
 fun implode_param [s, "?"] = s ^ "?"
   | implode_param [s, "!"] = s ^ "!"