# HG changeset patch # User wenzelm # Date 1398161038 -7200 # Node ID ca302c495bca3150a20a73acaf580cfbad5e6dd9 # Parent a2df9de46060b271dd15dfaa1e42ed58d05bb514 tuned; diff -r a2df9de46060 -r ca302c495bca src/Pure/Isar/isar_syn.ML --- a/src/Pure/Isar/isar_syn.ML Tue Apr 22 11:53:05 2014 +0200 +++ b/src/Pure/Isar/isar_syn.ML Tue Apr 22 12:03:58 2014 +0200 @@ -1021,7 +1021,7 @@ (Parse.opt_unit >> K (Toplevel.imperative Secure.commit)); val _ = - Outer_Syntax.improper_command @{command_spec "quit"} "quit Isabelle" + Outer_Syntax.improper_command @{command_spec "quit"} "quit Isabelle process" (Parse.opt_unit >> (K (Toplevel.imperative quit))); val _ =