remove needless exception
authorblanchet
Mon, 20 Sep 2010 16:31:47 +0200
changeset 39561 3857a4a81fa7
parent 39560 c13b4589fddf
child 39562 be44a81ca5ab
remove needless exception
src/HOL/Tools/Sledgehammer/clausifier.ML
--- a/src/HOL/Tools/Sledgehammer/clausifier.ML	Mon Sep 20 16:29:55 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/clausifier.ML	Mon Sep 20 16:31:47 2010 +0200
@@ -34,9 +34,6 @@
            Thm.instantiate ([], [(cterm_of @{theory HOL} v, ctp_false)]) th
     | _ => th
 
-(*To enforce single-threading*)
-exception Clausify_failure of theory;
-
 
 (**** SKOLEMIZATION BY INFERENCE (lcp) ****)