src/Pure/simplifier.ML

   Args.parens (Args.$$$ no_asm_simpN) >> K asm_simp_tac ||
   Args.parens (Args.$$$ no_asm_useN) >> K full_simp_tac ||
   Args.parens (Args.$$$ asm_lrN) >> K asm_lr_simp_tac ||
   Scan.succeed asm_full_simp_tac);
 
+val simp_flags = Scan.repeat
+  (Args.parens (Args.$$$ "depth_limit" -- Args.colon |-- Args.nat)
+    >> setmp MetaSimplifier.simp_depth_limit)
+  >> curry (Library.foldl op o) I;
+
 val cong_modifiers =
  [Args.$$$ congN -- Args.colon >> K ((I, cong_add_local):Method.modifier),
   Args.$$$ congN -- Args.add -- Args.colon >> K (I, cong_add_local),
   Args.$$$ congN -- Args.del -- Args.colon >> K (I, cong_del_local)];
 

   Args.del -- Args.colon >> K (I, simp_del_local),
   Args.$$$ onlyN -- Args.colon >> K (map_local_simpset clear_ss, simp_add_local)]
    @ cong_modifiers;
 
 fun simp_args more_mods =
-  Method.sectioned_args (Args.bang_facts -- Scan.lift simp_options) (more_mods @ simp_modifiers');
-
-
-fun simp_method (prems, tac) ctxt = Method.METHOD (fn facts =>
+  Method.sectioned_args (Args.bang_facts -- Scan.lift simp_options -- Scan.lift simp_flags)
+    (more_mods @ simp_modifiers');
+
+fun simp_method ((prems, tac), FLAGS) ctxt = Method.METHOD (fn facts =>
   ALLGOALS (Method.insert_tac (prems @ facts)) THEN
-    (CHANGED_PROP o ALLGOALS o tac) (local_simpset_of ctxt));
-
-fun simp_method' (prems, tac) ctxt = Method.METHOD (fn facts =>
+    (FLAGS o CHANGED_PROP o ALLGOALS o tac) (local_simpset_of ctxt));
+
+fun simp_method' ((prems, tac), FLAGS) ctxt = Method.METHOD (fn facts =>
   HEADGOAL (Method.insert_tac (prems @ facts) THEN'
-      (CHANGED_PROP oo tac) (local_simpset_of ctxt)));
+      ((FLAGS o CHANGED_PROP) oo tac) (local_simpset_of ctxt)));
 
 
 (* setup methods *)
 
 fun setup_methods more_mods = Method.add_methods