src/Pure/Isar/isar_cmd.ML
changeset 42464 ae16b8abf1a8
parent 42425 2aa907d5ee4f
child 43560 d1650e3720fd
     1.1 --- a/src/Pure/Isar/isar_cmd.ML	Sat Apr 23 13:00:19 2011 +0200
     1.2 +++ b/src/Pure/Isar/isar_cmd.ML	Sat Apr 23 13:53:09 2011 +0200
     1.3 @@ -20,8 +20,8 @@
     1.4    val add_defs: (bool * bool) * ((binding * string) * Attrib.src list) list -> theory -> theory
     1.5    val declaration: {syntax: bool, pervasive: bool} ->
     1.6      Symbol_Pos.text * Position.T -> local_theory -> local_theory
     1.7 -  val simproc_setup: string -> string list -> Symbol_Pos.text * Position.T -> string list ->
     1.8 -    local_theory -> local_theory
     1.9 +  val simproc_setup: string * Position.T -> string list -> Symbol_Pos.text * Position.T ->
    1.10 +    string list -> local_theory -> local_theory
    1.11    val hide_class: bool -> xstring list -> theory -> theory
    1.12    val hide_type: bool -> xstring list -> theory -> theory
    1.13    val hide_const: bool -> xstring list -> theory -> theory
    1.14 @@ -214,7 +214,7 @@
    1.15    ML_Lex.read pos txt
    1.16    |> ML_Context.expression pos
    1.17      "val proc: Morphism.morphism -> Simplifier.simpset -> cterm -> thm option"
    1.18 -    ("Context.map_proof (Simplifier.def_simproc {name = " ^ ML_Syntax.print_string name ^ ", \
    1.19 +    ("Context.map_proof (Simplifier.def_simproc_cmd {name = " ^ ML_Syntax.make_binding name ^ ", \
    1.20        \lhss = " ^ ML_Syntax.print_strings lhss ^ ", proc = proc, \
    1.21        \identifier = Library.maps ML_Context.thms " ^ ML_Syntax.print_strings identifier ^ "})")
    1.22    |> Context.proof_map;