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.
src/Pure/Isar/rule_cases.ML
changeset 15973 5fd94d84470f
parent 15574 b1d1b5bfc464
child 16148 5f15a14122dc 
--- a/src/Pure/Isar/rule_cases.ML	Tue May 17 10:19:43 2005 +0200
+++ b/src/Pure/Isar/rule_cases.ML	Tue May 17 10:19:44 2005 +0200
@@ -73,7 +73,7 @@
 
 fun get thm =
   let
-    val n = getOpt (lookup_consumes thm, 0);
+    val n = if_none (lookup_consumes thm) 0;
     val ss =
       (case lookup_case_names thm of
         NONE => map Library.string_of_int (1 upto (Thm.nprems_of thm - n))
isabelle