# HG changeset patch
# User haftmann
# Date 1325925138 -3600
# Node ID d6cafcc012ec541e578e83f95df27c17dd8ca453
# Parent  54ca5b2775a882c6ca363231e6ef390e62e380f3
tuned

diff -r 54ca5b2775a8 -r d6cafcc012ec src/HOL/Imperative_HOL/ex/SatChecker.thy
--- a/src/HOL/Imperative_HOL/ex/SatChecker.thy	Sat Jan 07 09:32:01 2012 +0100
+++ b/src/HOL/Imperative_HOL/ex/SatChecker.thy	Sat Jan 07 09:32:18 2012 +0100
@@ -5,7 +5,7 @@
 header {* An efficient checker for proofs from a SAT solver *}
 
 theory SatChecker
-imports "~~/src/HOL/Library/RBT_Impl" Sorted_List Imperative_HOL
+imports "~~/src/HOL/Library/RBT_Impl" Sorted_List "../Imperative_HOL"
 begin
 
 section{* General settings and functions for our representation of clauses *}
@@ -264,7 +264,7 @@
   case (3 l v va r)
   thus ?case
     unfolding resolve2.simps
-    by (fastforce dest!: res_mem simp add: merge_Nil)
+    by (fastforce dest!: res_mem)
 qed
 
 lemma res_thm'_Inv:
@@ -707,9 +707,10 @@
 code_type ProofStep
   (SML "MinisatProofStep.ProofStep")
 
-code_const ProofDone  and  Root              and  Conflict              and  Delete  and  Xstep
-     (SML "MinisatProofStep.ProofDone" and "MinisatProofStep.Root ((_),/ (_))" and "MinisatProofStep.Conflict ((_),/ (_))" and "MinisatProofStep.Delete" and "MinisatProofStep.Xstep ((_),/ (_))")
+code_const ProofDone and Root and Conflict and Delete and Xstep
+  (SML "MinisatProofStep.ProofDone" and "MinisatProofStep.Root ((_),/ (_))" and "MinisatProofStep.Conflict ((_),/ (_))" and "MinisatProofStep.Delete" and "MinisatProofStep.Xstep ((_),/ (_))")
 
 export_code checker tchecker lchecker in SML
 
 end
+