author | wenzelm |
Wed, 26 Apr 2006 22:40:46 +0200 | |
changeset 19476 | 816f519f8b72 |
parent 19475 | 8aa2b380614a |
child 19477 | a95176d0f0dd |
--- 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]);