# HG changeset patch
# User blanchet
# Date 1284993107 -7200
# Node ID 3857a4a81fa7811323199d71ac107ea8636b1598
# Parent  c13b4589fddf8f9277bdb11736dccfc0a9607e0e
remove needless exception

diff -r c13b4589fddf -r 3857a4a81fa7 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) ****)