# HG changeset patch
# User wenzelm
# Date 1284048275 -7200
# Node ID cda88e68106dd7b184085ecb5884cf65ed65861b
# Parent  d76a2fd129b521fe7eb92f9d49b2817c7525a572
Meson.make_clauses_unsorted: removed spurious debug code stemming from 5146d640aa4a -- must not handle arbitrary exceptions in user space;

diff -r d76a2fd129b5 -r cda88e68106d src/HOL/Tools/meson.ML
--- a/src/HOL/Tools/meson.ML	Thu Sep 09 18:00:16 2010 +0200
+++ b/src/HOL/Tools/meson.ML	Thu Sep 09 18:04:35 2010 +0200
@@ -575,8 +575,7 @@
 
 (*Make clauses from a list of theorems, previously Skolemized and put into nnf.
   The resulting clauses are HOL disjunctions.*)
-fun make_clauses_unsorted ths = fold_rev add_clauses ths []
-handle exn => error (ML_Compiler.exn_message exn) (*###*)
+fun make_clauses_unsorted ths = fold_rev add_clauses ths [];
 val make_clauses = sort_clauses o make_clauses_unsorted;
 
 (*Convert a list of clauses (disjunctions) to Horn clauses (contrapositives)*)