# HG changeset patch
# User blanchet
# Date 1286195655 -7200
# Node ID acde1b606b0eaae0393e30f9a69c9b31b5fac035
# Parent  97b8051033beb174a74fabc51262786e4a1b0802
reverted 0bfaaa81fc62, since "Thm.rename_boundvars" can't be relied upon to give unique names to bound variables

diff -r 97b8051033be -r acde1b606b0e src/HOL/Tools/Sledgehammer/meson_clausify.ML
--- a/src/HOL/Tools/Sledgehammer/meson_clausify.ML	Mon Oct 04 09:08:46 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/meson_clausify.ML	Mon Oct 04 14:34:15 2010 +0200
@@ -12,7 +12,7 @@
   val introduce_combinators_in_cterm : cterm -> thm
   val introduce_combinators_in_theorem : thm -> thm
   val to_definitional_cnf_with_quantifiers : theory -> thm -> thm
-  val cluster_of_zapped_var_name : string -> (int * int) * bool
+  val cluster_of_zapped_var_name : string -> (int * (int * int)) * bool
   val cnf_axiom :
     Proof.context -> bool -> int -> thm -> (thm * term) option * thm list
   val meson_general_tac : Proof.context -> thm list -> int -> tactic
@@ -229,64 +229,51 @@
     val eqth = eqth RS @{thm TruepropI}
   in Thm.equal_elim eqth th end
 
-fun zapped_var_name ax_no (cluster_no, skolem) s =
+fun zapped_var_name ((ax_no, cluster_no), skolem) index_no s =
   (if skolem then new_skolem_var_prefix else new_nonskolem_var_prefix) ^
-  "_" ^ string_of_int ax_no ^ "_" ^ string_of_int cluster_no ^ "_" ^ s
+  "_" ^ string_of_int ax_no ^ "_" ^ string_of_int cluster_no ^ "_" ^
+  string_of_int index_no ^ "_" ^ s
 
 fun cluster_of_zapped_var_name s =
-  ((1, 2) |> pairself (the o Int.fromString o nth (space_explode "_" s)),
-   String.isPrefix new_skolem_var_prefix s)
+  let val get_int = the o Int.fromString o nth (space_explode "_" s) in
+    ((get_int 1, (get_int 2, get_int 3)),
+     String.isPrefix new_skolem_var_prefix s)
+  end
 
-fun rename_vars_to_be_zapped ax_no =
-  let
-    fun aux (cluster as (cluster_no, cluster_skolem)) pos t =
-      case t of
-        (t1 as Const (s, _)) $ Abs (s', T, t') =>
-        if s = @{const_name all} orelse s = @{const_name All} orelse
-           s = @{const_name Ex} then
-          let
-            val skolem = (pos = (s = @{const_name Ex}))
-            val cluster =
-              if skolem = cluster_skolem then cluster
-              else (cluster_no |> cluster_skolem ? Integer.add 1, skolem)
-            val s' = zapped_var_name ax_no cluster s'
-          in t1 $ Abs (s', T, aux cluster pos t') end
-        else
-          t
-      | (t1 as Const (s, _)) $ t2 $ t3 =>
-        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 conj} orelse s = @{const_name disj} then
-          t1 $ aux cluster pos t2 $ aux cluster pos t3
-        else
-          t
-      | (t1 as Const (s, _)) $ t2 =>
-        if s = @{const_name Trueprop} then t1 $ aux cluster pos t2
-        else if s = @{const_name Not} then t1 $ aux cluster (not pos) t2
-        else t
-      | _ => t
-  in aux (0, true) true end
-
-fun zap pos ct =
+fun zap (cluster as (cluster_no, cluster_skolem)) index_no 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
+          let
+            val skolem = (pos = (s = @{const_name Ex}))
+            val (cluster, index_no) =
+              if skolem = cluster_skolem then (cluster, index_no)
+              else ((cluster_no ||> cluster_skolem ? Integer.add 1, skolem), 0)
+          in
+            Thm.dest_comb #> snd
+            #> Thm.dest_abs (SOME (zapped_var_name cluster index_no s'))
+            #> snd #> zap cluster (index_no + 1) pos
+          end
         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)
+          Conv.combination_conv (Conv.arg_conv (zap cluster index_no (not pos)))
+                                (zap cluster index_no pos)
         else if s = @{const_name conj} orelse s = @{const_name disj} then
-          Conv.combination_conv (Conv.arg_conv (zap pos)) (zap pos)
+          Conv.combination_conv (Conv.arg_conv (zap cluster index_no pos))
+                                (zap cluster index_no 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
+        if s = @{const_name Trueprop} then
+          Conv.arg_conv (zap cluster index_no pos)
+        else if s = @{const_name Not} then
+          Conv.arg_conv (zap cluster index_no (not pos))
+        else
+          Conv.all_conv
       | _ => Conv.all_conv)
 
 fun ss_only ths = MetaSimplifier.clear_ss HOL_basic_ss addsimps ths
@@ -311,10 +298,6 @@
   in
     if new_skolemizer then
       let
-        fun rename_bound_vars th =
-          let val t = concl_of th in
-            th |> Thm.rename_boundvars t (rename_vars_to_be_zapped ax_no t)
-          end
         fun skolemize choice_ths =
           Meson.skolemize_with_choice_thms ctxt choice_ths
           #> simplify (ss_only @{thms all_simps[symmetric]})
@@ -322,12 +305,12 @@
           simplify (ss_only @{thms all_simps[symmetric] ex_simps[symmetric]})
         val (discharger_th, fully_skolemized_th) =
           if null choice_ths then
-            th |> rename_bound_vars |> `I |>> pull_out ||> skolemize [no_choice]
+            th |> `I |>> pull_out ||> skolemize [no_choice]
           else
-            th |> skolemize choice_ths |> rename_bound_vars |> `I
+            th |> skolemize choice_ths |> `I
         val t =
           fully_skolemized_th |> cprop_of
-          |> zap true |> Drule.export_without_context
+          |> zap ((ax_no, 0), true) 0 true |> Drule.export_without_context
           |> cprop_of |> Thm.dest_equals |> snd |> term_of
       in
         if exists_subterm (fn Var ((s, _), _) =>