src/Pure/Isar/isar_cmd.ML

   val print_rules: Toplevel.transition -> Toplevel.transition
   val print_induct_rules: Toplevel.transition -> Toplevel.transition
   val print_trans_rules: Toplevel.transition -> Toplevel.transition
   val print_methods: Toplevel.transition -> Toplevel.transition
   val print_antiquotations: Toplevel.transition -> Toplevel.transition
-  val print_thms_containing: string list -> Toplevel.transition -> Toplevel.transition
+  val print_thms_containing: int option * string list
+    -> Toplevel.transition -> Toplevel.transition
   val thm_deps: (string * Args.src list) list -> Toplevel.transition -> Toplevel.transition
   val print_binds: Toplevel.transition -> Toplevel.transition
   val print_lthms: Toplevel.transition -> Toplevel.transition
   val print_cases: Toplevel.transition -> Toplevel.transition
   val print_thms: string list * (string * Args.src list) list

 val print_methods = Toplevel.unknown_theory o
   Toplevel.keep (Method.print_methods o Toplevel.theory_of);
 
 val print_antiquotations = Toplevel.imperative IsarOutput.print_antiquotations;
 
-fun print_thms_containing ss = Toplevel.unknown_theory o Toplevel.keep (fn state =>
+fun print_thms_containing (lim, spec) = Toplevel.unknown_theory o Toplevel.keep (fn state =>
   ProofContext.print_thms_containing
-    (Toplevel.node_case ProofContext.init Proof.context_of state) ss);
+    (Toplevel.node_case ProofContext.init Proof.context_of state) lim spec);
 
 fun thm_deps args = Toplevel.unknown_theory o Toplevel.keep (fn state =>
   ThmDeps.thm_deps (IsarThy.get_thmss args (Toplevel.enter_forward_proof state)));