Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Meson.make_clauses_unsorted: removed spurious debug code stemming from 5146d640aa4a -- must not handle arbitrary exceptions in user space;
authorwenzelm
Thu, 09 Sep 2010 18:04:35 +0200
changeset 39235 cda88e68106d
parent 39234 d76a2fd129b5
child 39236 2ec7afadc344
Meson.make_clauses_unsorted: removed spurious debug code stemming from 5146d640aa4a -- must not handle arbitrary exceptions in user space;
src/HOL/Tools/meson.ML file | annotate | diff | comparison | revisions 
--- 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)*)
isabelle