# HG changeset patch
# User wenzelm
# Date 1146084046 -7200
# Node ID 816f519f8b72c1f60576a4c063df9f29e279f04b
# Parent  8aa2b380614a2f710a67f87616c1bc188b9342de
*** empty log message ***

diff -r 8aa2b380614a -r 816f519f8b72 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]);