Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
TFL/casesplit.ML
changeset 21858 05f57309170c
parent 21708 45e7491bea47
child 22578 b0eb5652f210 
--- a/TFL/casesplit.ML	Thu Dec 14 22:19:39 2006 +0100
+++ b/TFL/casesplit.ML	Fri Dec 15 00:08:06 2006 +0100
@@ -268,7 +268,7 @@
 having to (re)search for variables to split. *)
 fun splitto splitths genth =
     let
-      val _ = assert (not (null splitths)) "splitto: no given splitths";
+      val _ = not (null splitths) orelse error "splitto: no given splitths";
       val sgn = Thm.sign_of_thm genth;
 
       (* check if we are a member of splitths - FIXME: quicker and
isabelle