diff -r adc1143bc1a8 -r 4c0a5e35931a src/HOL/Imperative_HOL/ex/SatChecker.thy
--- a/src/HOL/Imperative_HOL/ex/SatChecker.thy	Wed Jul 14 16:02:50 2010 +0200
+++ b/src/HOL/Imperative_HOL/ex/SatChecker.thy	Wed Jul 14 16:13:14 2010 +0200
@@ -710,8 +710,6 @@
 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 in SML module_name SAT file -
-export_code tchecker in SML module_name SAT file -
-export_code lchecker in SML module_name SAT file -
+export_code checker tchecker lchecker in SML
 
 end