src/Pure/Isar/isar_cmd.ML
changeset 61144 5e94dfead1c2
parent 61086 fc7ab11128dc
child 61266 eb9522a9d997
     1.1 --- a/src/Pure/Isar/isar_cmd.ML	Wed Sep 09 14:47:41 2015 +0200
     1.2 +++ b/src/Pure/Isar/isar_cmd.ML	Wed Sep 09 20:57:21 2015 +0200
     1.3 @@ -168,8 +168,9 @@
     1.4    ML_Lex.read_source false source
     1.5    |> ML_Context.expression (Input.range_of source) "proc"
     1.6      "Morphism.morphism -> Proof.context -> cterm -> thm option"
     1.7 -    ("Context.map_proof (Simplifier.def_simproc_cmd {name = " ^ ML_Syntax.make_binding name ^ ", \
     1.8 -      \lhss = " ^ ML_Syntax.print_strings lhss ^ ", proc = proc, \
     1.9 +    ("Context.map_proof (Simplifier.define_simproc_cmd " ^
    1.10 +      ML_Syntax.atomic (ML_Syntax.make_binding name) ^
    1.11 +      "{lhss = " ^ ML_Syntax.print_strings lhss ^ ", proc = proc, \
    1.12        \identifier = Library.maps ML_Context.thms " ^ ML_Syntax.print_strings identifier ^ "})")
    1.13    |> Context.proof_map;
    1.14