# HG changeset patch
# User wenzelm
# Date 918056882 -3600
# Node ID 451d3d6c088f93d01de709257f6fa12546de3a9f
# Parent  a42dbf1af868f7e7c808e14bad1e49d33cb73c72
removed load;

diff -r a42dbf1af868 -r 451d3d6c088f src/Pure/Isar/isar.ML
--- a/src/Pure/Isar/isar.ML	Wed Feb 03 16:47:37 1999 +0100
+++ b/src/Pure/Isar/isar.ML	Wed Feb 03 16:48:02 1999 +0100
@@ -11,7 +11,6 @@
   val main: unit -> unit
   val loop: unit -> unit
   val help: unit -> unit
-  val load: string -> unit
   val commands: unit -> string list
   val add_keywords: string list -> unit
   val add_parsers: parser list -> unit
@@ -24,7 +23,6 @@
 val main = OuterSyntax.main;
 val loop = OuterSyntax.loop;
 val help = OuterSyntax.help;
-val load = OuterSyntax.load;
 val commands = OuterSyntax.commands;
 val add_keywords = OuterSyntax.add_keywords;
 val add_parsers = OuterSyntax.add_parsers;