# HG changeset patch
# User blanchet
# Date 1292408789 -3600
# Node ID 9aeaf8acf6c864d4412d555b368e31f751113413
# Parent  85da8cbb496681a458cd266fb72e5d97647a6e07
tuning

diff -r 85da8cbb4966 -r 9aeaf8acf6c8 src/HOL/Tools/Metis/metis_translate.ML
--- a/src/HOL/Tools/Metis/metis_translate.ML	Wed Dec 15 11:26:29 2010 +0100
+++ b/src/HOL/Tools/Metis/metis_translate.ML	Wed Dec 15 11:26:29 2010 +0100
@@ -114,20 +114,20 @@
                (@{const_name disj}, "disj"),
                (@{const_name implies}, "implies"),
                (@{const_name HOL.eq}, "equal"),
+               (@{const_name If}, "If"),
                (@{const_name Set.member}, "member"),
+               (@{const_name Meson.COMBI}, "COMBI"),
+               (@{const_name Meson.COMBK}, "COMBK"),
+               (@{const_name Meson.COMBB}, "COMBB"),
+               (@{const_name Meson.COMBC}, "COMBC"),
+               (@{const_name Meson.COMBS}, "COMBS"),
                (@{const_name Metis.fFalse}, "fFalse"),
                (@{const_name Metis.fTrue}, "fTrue"),
                (@{const_name Metis.fNot}, "fNot"),
                (@{const_name Metis.fconj}, "fconj"),
                (@{const_name Metis.fdisj}, "fdisj"),
                (@{const_name Metis.fimplies}, "fimplies"),
-               (@{const_name Metis.fequal}, "fequal"),
-               (@{const_name Meson.COMBI}, "COMBI"),
-               (@{const_name Meson.COMBK}, "COMBK"),
-               (@{const_name Meson.COMBB}, "COMBB"),
-               (@{const_name Meson.COMBC}, "COMBC"),
-               (@{const_name Meson.COMBS}, "COMBS"),
-               (@{const_name If}, "If")]
+               (@{const_name Metis.fequal}, "fequal")]
 
 (* Invert the table of translations between Isabelle and ATPs. *)
 val const_trans_table_inv =
@@ -692,10 +692,9 @@
     (false, @{lemma "~ P | fdisj P Q" "~ Q | fdisj P Q" "~ fdisj P Q | P | Q"
               by (unfold fdisj_def) fast+})),
    ("c_fimplies",
-    (false, @{lemma "P | Metis.fimplies P Q"
-                    "~ Q | Metis.fimplies P Q"
-                    "~ Metis.fimplies P Q | ~ P | Q"
-              by (unfold Metis.fimplies_def) fast+})),
+    (false, @{lemma "P | fimplies P Q" "~ Q | fimplies P Q"
+                    "~ fimplies P Q | ~ P | Q"
+              by (unfold fimplies_def) fast+})),
    ("c_If", (true, @{thms if_True if_False True_or_False})) (* FIXME *)]
 
 (* ------------------------------------------------------------------------- *)
@@ -732,9 +731,9 @@
 fun const_in_metis c (pred, tm_list) =
   let
     fun in_mterm (Metis_Term.Var _) = false
-      | in_mterm (Metis_Term.Fn (".", tm_list)) = exists in_mterm tm_list
-      | in_mterm (Metis_Term.Fn (nm, tm_list)) = c=nm orelse exists in_mterm tm_list
-  in  c = pred orelse exists in_mterm tm_list  end;
+      | in_mterm (Metis_Term.Fn (nm, tm_list)) =
+        c = nm orelse exists in_mterm tm_list
+  in c = pred orelse exists in_mterm tm_list end
 
 (* ARITY CLAUSE *)
 fun m_arity_cls (TConsLit ((c, _), (t, _), args)) =
@@ -794,9 +793,8 @@
           lmap
         else
           let
-            val fdefs = @{thms Metis.fFalse_def Metis.fTrue_def Metis.fNot_def
-                               Metis.fconj_def Metis.fdisj_def
-                               Metis.fimplies_def Metis.fequal_def}
+            val fdefs = @{thms fFalse_def fTrue_def fNot_def fconj_def fdisj_def
+                               fimplies_def fequal_def}
             val prepare_helper =
               zero_var_indexes
               #> `(Meson.make_meta_clause