# HG changeset patch
# User wenzelm
# Date 1087411003 -7200
# Node ID f1789e22ceec957202d0f6995444fd116c11ecc1
# Parent  27decf8d40ffd2299540ec827727122feda099b8
removed unused help function;

diff -r 27decf8d40ff -r f1789e22ceec src/Pure/Isar/outer_syntax.ML
--- a/src/Pure/Isar/outer_syntax.ML	Wed Jun 16 14:56:58 2004 +0200
+++ b/src/Pure/Isar/outer_syntax.ML	Wed Jun 16 20:36:43 2004 +0200
@@ -388,13 +388,6 @@
 fun sync_loop () = gen_loop true true;
 
 
-(* help *)
-
-fun help () =
-  writeln ("This is Isabelle's underlying ML system (" ^ ml_system ^ ");\n\
-    \invoke 'Isar.loop();' to get back to the Isar read-eval-print loop.");
-
-
 (*final declarations of this structure!*)
 val command = parser false None;
 val markup_command = parser false o Some;