# HG changeset patch
# User wenzelm
# Date 930738165 -7200
# Node ID 5906a7929b856f48e89dee9cedbd725fa342d14c
# Parent  6e6eb8d92377e7acaba9953da32d5445a402bc2f
sync;

diff -r 6e6eb8d92377 -r 5906a7929b85 src/Pure/Isar/isar.ML
--- a/src/Pure/Isar/isar.ML	Wed Jun 30 12:22:31 1999 +0200
+++ b/src/Pure/Isar/isar.ML	Wed Jun 30 12:22:45 1999 +0200
@@ -9,6 +9,8 @@
 sig
   val main: unit -> unit
   val loop: unit -> unit
+  val sync_main: unit -> unit
+  val sync_loop: unit -> unit
   val help: unit -> unit
 end;
 
@@ -17,6 +19,8 @@
 
 val main = OuterSyntax.main;
 val loop = OuterSyntax.loop;
+val sync_main = OuterSyntax.sync_main;
+val sync_loop = OuterSyntax.sync_loop;
 val help = OuterSyntax.help;
 
 end;