src/Pure/Isar/isar_cmd.ML

   val print_ast_translation: Input.source -> theory -> theory
   val translations: (xstring * string) Syntax.trrule list -> theory -> theory
   val no_translations: (xstring * string) Syntax.trrule list -> theory -> theory
   val oracle: bstring * Position.range -> Input.source -> theory -> theory
   val declaration: {syntax: bool, pervasive: bool} -> Input.source -> local_theory -> local_theory
-  val simproc_setup: string * Position.T -> string list -> Input.source ->
+  val simproc_setup: string * Position.T -> string list -> Input.source -> bool ->
     local_theory -> local_theory
   val qed: Method.text_range option -> Toplevel.transition -> Toplevel.transition
   val terminal_proof: Method.text_range * Method.text_range option ->
     Toplevel.transition -> Toplevel.transition
   val default_proof: Toplevel.transition -> Toplevel.transition

   |> Context.proof_map;
 
 
 (* simprocs *)
 
-fun simproc_setup name lhss source =
+fun simproc_setup name lhss source passive =
   ML_Context.expression (Input.pos_of source)
     (ML_Lex.read
       ("Theory.local_setup (Simplifier.define_simproc_cmd (" ^
         ML_Syntax.make_binding name ^ ") {lhss = " ^ ML_Syntax.print_strings lhss ^
+        ", passive = " ^ Bool.toString passive ^
         ", proc = (") @ ML_Lex.read_source source @ ML_Lex.read ")})")
   |> Context.proof_map;
 
 
 (* local endings *)