fix cluster numbering in the absense of Hilbert_Choice (reverts acde1b606b0e, effectively reintroducing most of 0bfaaa81fc62)

--- a/src/HOL/Tools/Meson/meson_clausify.ML	Fri Oct 29 12:49:05 2010 +0200
+++ b/src/HOL/Tools/Meson/meson_clausify.ML	Fri Oct 29 12:49:05 2010 +0200
@@ -241,10 +241,11 @@
      String.isPrefix new_skolem_var_prefix s)
   end
 
-fun zap (cluster as (cluster_no, cluster_skolem)) index_no pos ct =
-  ct
-  |> (case term_of ct of
-        Const (s, _) $ Abs (s', _, _) =>
+fun rename_bound_vars_to_be_zapped ax_no =
+  let
+    fun aux (cluster as (cluster_no, cluster_skolem)) index_no 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
@@ -252,29 +253,48 @@
             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
+            val s' = zapped_var_name cluster index_no s'
+          in t1 $ Abs (s', T, aux cluster (index_no + 1) pos t') end
+        else
+          t
+      | (t1 as Const (s, _)) $ t2 $ t3 =>
+        if s = @{const_name "==>"} orelse s = @{const_name HOL.implies} then
+          t1 $ aux cluster index_no (not pos) t2 $ aux cluster index_no pos t3
+        else if s = @{const_name HOL.conj} orelse
+                s = @{const_name HOL.disj} then
+          t1 $ aux cluster index_no pos t2 $ aux cluster index_no pos t3
+        else
+          t
+      | (t1 as Const (s, _)) $ t2 =>
+        if s = @{const_name Trueprop} then
+          t1 $ aux cluster index_no pos t2
+        else if s = @{const_name Not} then
+          t1 $ aux cluster index_no (not pos) t2
+        else
+          t
+      | _ => t
+  in aux ((ax_no, 0), true) 0 true 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 cluster index_no (not pos)))
-                                (zap cluster index_no pos)
+          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 cluster index_no pos))
-                                (zap cluster index_no pos)
+          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 cluster index_no pos)
-        else if s = @{const_name Not} then
-          Conv.arg_conv (zap cluster index_no (not pos))
-        else
-          Conv.all_conv
+        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
@@ -304,24 +324,25 @@
           #> simplify (ss_only @{thms all_simps[symmetric]})
         val pull_out =
           simplify (ss_only @{thms all_simps[symmetric] ex_simps[symmetric]})
-        val (discharger_th, fully_skolemized_th) =
-          if null choice_ths then
-            th |> `I |>> pull_out ||> skolemize [no_choice]
-          else
-            th |> skolemize choice_ths |> `I
-        val t =
-          fully_skolemized_th |> cprop_of
-          |> zap ((ax_no, 0), true) 0 true |> Drule.export_without_context
-          |> cprop_of |> Thm.dest_equals |> snd |> term_of
+        val discharger_th =
+          th |> (if null choice_ths then pull_out else skolemize choice_ths)
+        val fully_skolemized_t =
+          th |> prop_of |> rename_bound_vars_to_be_zapped ax_no
+             |> Skip_Proof.make_thm thy |> skolemize [no_choice] |> 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
-                            | _ => false) t then
+                            | _ => false) fully_skolemized_t then
           let
-            val (ct, ctxt) =
-              Variable.import_terms true [t] ctxt
+            val (fully_skolemized_ct, ctxt) =
+              Variable.import_terms true [fully_skolemized_t] ctxt
               |>> the_single |>> cterm_of thy
-          in (SOME (discharger_th, ct), Thm.assume ct, ctxt) end
+          in
+            (SOME (discharger_th, fully_skolemized_ct),
+                   Thm.assume fully_skolemized_ct, ctxt)
+          end
        else
          (NONE, th, ctxt)
       end