--- a/src/Pure/Tools/find_theorems.ML Wed Dec 06 15:46:35 2017 +0100
+++ b/src/Pure/Tools/find_theorems.ML Wed Dec 06 18:59:33 2017 +0100
@@ -190,7 +190,7 @@
val goal' = Thm.transfer thy' goal;
fun limited_etac thm i =
- Seq.take (Options.default_int @{system_option find_theorems_tactic_limit}) o
+ Seq.take (Options.default_int \<^system_option>\<open>find_theorems_tactic_limit\<close>) o
eresolve_tac ctxt' [thm] i;
fun try_thm thm =
if Thm.no_prems thm then resolve_tac ctxt' [thm] 1 goal'
@@ -414,7 +414,7 @@
else raw_matches;
val len = length matches;
- val lim = the_default (Options.default_int @{system_option find_theorems_limit}) opt_limit;
+ val lim = the_default (Options.default_int \<^system_option>\<open>find_theorems_limit\<close>) opt_limit;
in (SOME len, drop (Int.max (len - lim, 0)) matches) end;
val find =