src/Pure/Isar/isar_cmd.ML
changeset 51717 9e7d1c139569
parent 51583 9100c8e66b69
child 52143 36ffe23b25f8
     1.1 --- a/src/Pure/Isar/isar_cmd.ML	Tue Apr 16 17:54:14 2013 +0200
     1.2 +++ b/src/Pure/Isar/isar_cmd.ML	Thu Apr 18 17:07:01 2013 +0200
     1.3 @@ -193,7 +193,7 @@
     1.4  fun simproc_setup name lhss (txt, pos) identifier =
     1.5    ML_Lex.read pos txt
     1.6    |> ML_Context.expression pos
     1.7 -    "val proc: Morphism.morphism -> Simplifier.simpset -> cterm -> thm option"
     1.8 +    "val proc: Morphism.morphism -> Proof.context -> cterm -> thm option"
     1.9      ("Context.map_proof (Simplifier.def_simproc_cmd {name = " ^ ML_Syntax.make_binding name ^ ", \
    1.10        \lhss = " ^ ML_Syntax.print_strings lhss ^ ", proc = proc, \
    1.11        \identifier = Library.maps ML_Context.thms " ^ ML_Syntax.print_strings identifier ^ "})")