*** empty log message ***
authorwenzelm
Wed, 26 Apr 2006 22:40:46 +0200
changeset 19476 816f519f8b72
parent 19475 8aa2b380614a
child 19477 a95176d0f0dd
*** empty log message ***
src/Pure/Isar/find_theorems.ML
--- a/src/Pure/Isar/find_theorems.ML	Wed Apr 26 22:38:16 2006 +0200
+++ b/src/Pure/Isar/find_theorems.ML	Wed Apr 26 22:40:46 2006 +0200
@@ -252,7 +252,7 @@
 
     val matches = all_filters filters (find_thms ctxt ([], []));
     val len = length matches;
-    val limit = if_none opt_limit (! thms_containing_limit);
+    val limit = the_default (! thms_containing_limit) opt_limit;
 
     fun prt_fact (thmref, thm) =
       ProofContext.pretty_fact ctxt (PureThy.string_of_thmref thmref, [thm]);