# HG changeset patch
# User blanchet
# Date 1292408788 -3600
# Node ID 0b05cc14c2cb482447bb70c3aa7ed548a2bdb805
# Parent  43e2b051339c51f87836b18581881e3d999e8faf
remove at most one double negation -- any other double negations are part of some higher-order reasoning and should be left alone, cf. "HO_Reas.thy"

diff -r 43e2b051339c -r 0b05cc14c2cb src/HOL/Tools/Metis/metis_reconstruct.ML
--- a/src/HOL/Tools/Metis/metis_reconstruct.ML	Wed Dec 15 11:26:28 2010 +0100
+++ b/src/HOL/Tools/Metis/metis_reconstruct.ML	Wed Dec 15 11:26:28 2010 +0100
@@ -373,13 +373,16 @@
       else raise THM("select_literal", i, [th])
   end;
 
+val neg_neg_imp = @{lemma "~ ~ Q ==> Q" by blast}
+
 (* Maps a rule that ends "... ==> P ==> False" to "... ==> ~P" while suppressing
    double-negations. *)
-val negate_head =
-  fold (rewrite_rule o single) [@{thm atomize_not}, not_not RS eq_reflection]
+fun negate_head thy =
+  rewrite_rule @{thms atomize_not}
+  #> perhaps (try (fn th => resolve_inc_tyvars thy th 1 neg_neg_imp))
 
 (* Maps the clause  [P1,...Pn]==>False to [P1,...,P(i-1),P(i+1),...Pn] ==> ~P *)
-val select_literal = negate_head oo make_last
+fun select_literal thy = negate_head thy oo make_last
 
 fun resolve_inf ctxt mode skolem_params thpairs atm th1 th2 =
   let
@@ -410,7 +413,8 @@
           handle Empty => raise Fail "Failed to find literal in th2"
         val _ = trace_msg ctxt (fn () => "  index_th2: " ^ Int.toString index_th2)
     in
-      resolve_inc_tyvars thy (select_literal index_th1 i_th1) index_th2 i_th2
+      resolve_inc_tyvars thy (select_literal thy index_th1 i_th1) index_th2
+                         i_th2
     end
   end;