# HG changeset patch
# User wenzelm
# Date 933105539 -7200
# Node ID 247e4247b64e4138423f347966ee1013ec7dab65
# Parent  1c44df10a7bc538f98a774258c94b89c60212ffe
added thy_switch kind;

diff -r 1c44df10a7bc -r 247e4247b64e src/Pure/Isar/outer_syntax.ML
--- a/src/Pure/Isar/outer_syntax.ML	Tue Jul 27 21:58:39 1999 +0200
+++ b/src/Pure/Isar/outer_syntax.ML	Tue Jul 27 21:58:59 1999 +0200
@@ -22,6 +22,7 @@
       val control: string
       val diag: string
       val thy_begin: string
+      val thy_switch: string
       val thy_end: string
       val thy_heading: string
       val thy_decl: string
@@ -68,6 +69,7 @@
   val control = "control";
   val diag = "diag";
   val thy_begin = "theory-begin";
+  val thy_switch = "theory-switch";
   val thy_end = "theory-end";
   val thy_heading = "theory-heading";
   val thy_decl = "theory-decl";
@@ -81,8 +83,8 @@
   val prf_asm = "proof-asm";
   val prf_script = "proof-script";
 
-  val kinds = [control, diag, thy_begin, thy_end, thy_heading, thy_decl, thy_goal, qed,
-    qed_block, prf_goal, prf_block, prf_chain, prf_decl, prf_asm, prf_script];
+  val kinds = [control, diag, thy_begin, thy_switch, thy_end, thy_heading, thy_decl, thy_goal,
+    qed, qed_block, prf_goal, prf_block, prf_chain, prf_decl, prf_asm, prf_script];
 end;