src/Pure/Isar/isar_cmd.ML
changeset 62913 13252110a6fe
parent 62169 a6047f511de7
child 62922 96691631c1eb
     1.1 --- a/src/Pure/Isar/isar_cmd.ML	Thu Apr 07 22:09:23 2016 +0200
     1.2 +++ b/src/Pure/Isar/isar_cmd.ML	Fri Apr 08 20:15:20 2016 +0200
     1.3 @@ -18,7 +18,7 @@
     1.4    val oracle: bstring * Position.range -> Input.source -> theory -> theory
     1.5    val declaration: {syntax: bool, pervasive: bool} -> Input.source -> local_theory -> local_theory
     1.6    val simproc_setup: string * Position.T -> string list -> Input.source ->
     1.7 -    string list -> local_theory -> local_theory
     1.8 +    local_theory -> local_theory
     1.9    val qed: Method.text_range option -> Toplevel.transition -> Toplevel.transition
    1.10    val terminal_proof: Method.text_range * Method.text_range option ->
    1.11      Toplevel.transition -> Toplevel.transition
    1.12 @@ -151,14 +151,13 @@
    1.13  
    1.14  (* simprocs *)
    1.15  
    1.16 -fun simproc_setup name lhss source identifier =
    1.17 +fun simproc_setup name lhss source =
    1.18    ML_Lex.read_source false source
    1.19    |> ML_Context.expression (Input.range_of source) "proc"
    1.20      "Morphism.morphism -> Proof.context -> cterm -> thm option"
    1.21      ("Context.map_proof (Simplifier.define_simproc_cmd " ^
    1.22        ML_Syntax.atomic (ML_Syntax.make_binding name) ^
    1.23 -      "{lhss = " ^ ML_Syntax.print_strings lhss ^ ", proc = proc, \
    1.24 -      \identifier = Library.maps ML_Context.thms " ^ ML_Syntax.print_strings identifier ^ "})")
    1.25 +      "{lhss = " ^ ML_Syntax.print_strings lhss ^ ", proc = proc})")
    1.26    |> Context.proof_map;
    1.27  
    1.28