# HG changeset patch
# User blanchet
# Date 1302773045 -7200
# Node ID 187354e22c7d69d13784269e2f75868f6fd3e61e
# Parent  53e444ecb525d5aa1b13bb9e8b303ac8454af61b
improve on 0b05cc14c2cb: make sure that a literal variable "?foo" isn't accidentally renamed "?Q", which might be enough to confuse the new Skolemizer (cf. "Clausify.thy" example)

diff -r 53e444ecb525 -r 187354e22c7d src/HOL/Tools/Metis/metis_reconstruct.ML
--- a/src/HOL/Tools/Metis/metis_reconstruct.ML	Thu Apr 14 11:24:05 2011 +0200
+++ b/src/HOL/Tools/Metis/metis_reconstruct.ML	Thu Apr 14 11:24:05 2011 +0200
@@ -380,14 +380,16 @@
 
 val neg_neg_imp = @{lemma "~ ~ Q ==> Q" by blast}
 
-(* Maps a rule that ends "... ==> P ==> False" to "... ==> ~P" while suppressing
-   double-negations. *)
-fun negate_head thy =
-  rewrite_rule @{thms atomize_not}
-  #> perhaps (try (fn th => resolve_inc_tyvars thy th 1 neg_neg_imp))
+val not_atomize =
+  @{lemma "(~ A ==> False) == Trueprop A"
+    by (cut_tac atomize_not [of "~ A"]) simp}
+
+(* Maps a rule that ends "... ==> P ==> False" to "... ==> ~ P" while avoiding
+   to create double negations. *)
+val negate_head = fold (rewrite_rule o single) [not_atomize, atomize_not]
 
 (* Maps the clause  [P1,...Pn]==>False to [P1,...,P(i-1),P(i+1),...Pn] ==> ~P *)
-fun select_literal thy = negate_head thy oo make_last
+val select_literal = negate_head oo make_last
 
 fun resolve_inf ctxt mode skolem_params thpairs atm th1 th2 =
   let
@@ -418,8 +420,7 @@
           handle Empty => raise Fail "Failed to find literal in th2"
         val _ = trace_msg ctxt (fn () => "  index_th2: " ^ string_of_int index_th2)
     in
-      resolve_inc_tyvars thy (select_literal thy index_th1 i_th1) index_th2
-                         i_th2
+      resolve_inc_tyvars thy (select_literal index_th1 i_th1) index_th2 i_th2
     end
   end;