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.
remove debugging code
authorblanchet
Fri, 23 Apr 2010 16:59:48 +0200
changeset 36374 19c0c4b8b445
parent 36373 66af0a49de39
child 36375 2482446a604c
remove debugging code
src/HOL/Tools/refute.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/Tools/refute.ML	Fri Apr 23 16:55:51 2010 +0200
+++ b/src/HOL/Tools/refute.ML	Fri Apr 23 16:59:48 2010 +0200
@@ -1357,7 +1357,6 @@
     val subst_t = Term.subst_bounds (map Free frees, strip_t)
   in
     find_model thy (actual_params thy params) assm_ts subst_t true
-    handle REFUTE (s, s') => error ("REFUTE " ^ s ^ " " ^ s') (* ### *)
   end;
 
 (* ------------------------------------------------------------------------- *)
isabelle