# HG changeset patch
# User blanchet
# Date 1285948340 -7200
# Node ID 864bfafcf2510d6a4f7c1a08e3884d96ee78cada
# Parent  0bfaaa81fc62970d2d3dfc3ffd4c321b964f9fbd
tuning

diff -r 0bfaaa81fc62 -r 864bfafcf251 src/HOL/Tools/Sledgehammer/meson_clausify.ML
--- a/src/HOL/Tools/Sledgehammer/meson_clausify.ML	Fri Oct 01 17:41:59 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/meson_clausify.ML	Fri Oct 01 17:52:20 2010 +0200
@@ -73,8 +73,8 @@
         (*Universal quant: insert a free variable into body and continue*)
         let val fname = Name.variant (OldTerm.add_term_names (p,[])) a
         in dec_sko (subst_bound (Free(fname,T), p)) rhss end
-      | dec_sko (@{const HOL.conj} $ p $ q) rhss = rhss |> dec_sko p |> dec_sko q
-      | dec_sko (@{const HOL.disj} $ p $ q) rhss = rhss |> dec_sko p |> dec_sko q
+      | dec_sko (@{const conj} $ p $ q) rhss = rhss |> dec_sko p |> dec_sko q
+      | dec_sko (@{const disj} $ p $ q) rhss = rhss |> dec_sko p |> dec_sko q
       | dec_sko (@{const Trueprop} $ p) rhss = dec_sko p rhss
       | dec_sko _ rhss = rhss
   in  dec_sko (prop_of th) []  end;
@@ -255,11 +255,9 @@
         else
           t
       | (t1 as Const (s, _)) $ t2 $ t3 =>
-        if s = @{const_name "==>"} orelse
-           s = @{const_name HOL.implies} then
+        if s = @{const_name "==>"} orelse s = @{const_name implies} then
           t1 $ aux cluster (not pos) t2 $ aux cluster pos t3
-        else if s = @{const_name HOL.conj} orelse
-                s = @{const_name HOL.disj} then
+        else if s = @{const_name conj} orelse s = @{const_name disj} then
           t1 $ aux cluster pos t2 $ aux cluster pos t3
         else
           t
@@ -270,36 +268,27 @@
       | _ => t
   in aux (0, true) true end
 
-val zap_quantifiers =
-  let
-    fun conv pos ct =
-      ct |> (case term_of ct of
-               Const (s, _) $ Abs (s', _, _) =>
-               if s = @{const_name all} orelse s = @{const_name All} orelse
-                  s = @{const_name Ex} then
-                 Thm.dest_comb #> snd #> Thm.dest_abs (SOME s') #> snd
-                 #> conv pos
-               else
-                 Conv.all_conv
-             | Const (s, _) $ _ $ _ =>
-               if s = @{const_name "==>"} orelse
-                  s = @{const_name HOL.implies} then
-                 Conv.combination_conv (Conv.arg_conv (conv (not pos)))
-                                       (conv pos)
-               else if s = @{const_name HOL.conj} orelse
-                       s = @{const_name HOL.disj} then
-                 Conv.combination_conv (Conv.arg_conv (conv pos)) (conv pos)
-               else
-                 Conv.all_conv
-             | Const (s, _) $ _ =>
-               if s = @{const_name Trueprop} then Conv.arg_conv (conv pos)
-               else if s = @{const_name Not} then Conv.arg_conv (conv (not pos))
-               else Conv.all_conv
-             | _ => Conv.all_conv)
-  in
-    conv true #> Drule.export_without_context
-    #> cprop_of #> Thm.dest_equals #> snd
-  end
+fun zap pos ct =
+  ct
+  |> (case term_of ct of
+        Const (s, _) $ Abs (s', _, _) =>
+        if s = @{const_name all} orelse s = @{const_name All} orelse
+           s = @{const_name Ex} then
+          Thm.dest_comb #> snd #> Thm.dest_abs (SOME s') #> snd #> zap pos
+        else
+          Conv.all_conv
+      | Const (s, _) $ _ $ _ =>
+        if s = @{const_name "==>"} orelse s = @{const_name implies} then
+          Conv.combination_conv (Conv.arg_conv (zap (not pos))) (zap pos)
+        else if s = @{const_name conj} orelse s = @{const_name disj} then
+          Conv.combination_conv (Conv.arg_conv (zap pos)) (zap pos)
+        else
+          Conv.all_conv
+      | Const (s, _) $ _ =>
+        if s = @{const_name Trueprop} then Conv.arg_conv (zap pos)
+        else if s = @{const_name Not} then Conv.arg_conv (zap (not pos))
+        else Conv.all_conv
+      | _ => Conv.all_conv)
 
 fun ss_only ths = MetaSimplifier.clear_ss HOL_basic_ss addsimps ths
 
@@ -336,7 +325,9 @@
           else
             th |> skolemize choice_ths |> `I
         val t =
-          fully_skolemized_th |> cprop_of |> zap_quantifiers |> term_of
+          fully_skolemized_th |> cprop_of
+          |> zap true |> Drule.export_without_context
+          |> cprop_of |> Thm.dest_equals |> snd |> term_of
       in
         if exists_subterm (fn Var ((s, _), _) =>
                               String.isPrefix new_skolem_var_prefix s