src/Pure/Tools/find_theorems.ML

       |> Context_Position.set_visible_global (Context_Position.is_visible ctxt);
     val ctxt' = Proof_Context.transfer thy' ctxt;
     val goal' = Thm.transfer thy' goal;
 
     fun limited_etac thm i =
-      Seq.take (Options.default_int @{option find_theorems_tac_limit}) o etac thm i;
+      Seq.take (Options.default_int @{system_option find_theorems_tac_limit}) o etac thm i;
     fun try_thm thm =
       if Thm.no_prems thm then rtac thm 1 goal'
       else
         (limited_etac thm THEN_ALL_NEW (Goal.norm_hhf_tac ctxt' THEN' Method.assm_tac ctxt'))
           1 goal';

           if rem_dups
           then rem_thm_dups (nicer_shortest ctxt) raw_matches
           else raw_matches;
 
         val len = length matches;
-        val lim = the_default (Options.default_int @{option find_theorems_limit}) opt_limit;
+        val lim = the_default (Options.default_int @{system_option find_theorems_limit}) opt_limit;
       in (SOME len, drop (Int.max (len - lim, 0)) matches) end;
 
     val find =
       if rem_dups orelse is_none opt_limit
       then find_all