# HG changeset patch
# User wenzelm
# Date 962473345 -7200
# Node ID fdecb23119c0c04d9283786b9b78f2155927f205
# Parent  adef902823f95572e9223f3cae814f001795f840
removed help;

diff -r adef902823f9 -r fdecb23119c0 src/Pure/Isar/isar.ML
--- a/src/Pure/Isar/isar.ML	Sat Jul 01 19:42:08 2000 +0200
+++ b/src/Pure/Isar/isar.ML	Sat Jul 01 19:42:25 2000 +0200
@@ -12,7 +12,6 @@
   val loop: unit -> unit
   val sync_main: unit -> unit
   val sync_loop: unit -> unit
-  val help: unit -> unit
 end;
 
 structure Isar: ISAR =
@@ -22,6 +21,5 @@
 val loop = OuterSyntax.loop;
 val sync_main = OuterSyntax.sync_main;
 val sync_loop = OuterSyntax.sync_loop;
-val help = OuterSyntax.help;
 
 end;