# HG changeset patch
# User wenzelm
# Date 1163257903 -3600
# Node ID 7ab6e95e6b0b4bba32e0c5f3186edc74362cb132
# Parent  d41eddfd2b663e3738aed592c331607bc4e412c2
turned 'context' into plain thy_decl, discontinued thy_switch;

diff -r d41eddfd2b66 -r 7ab6e95e6b0b src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Sat Nov 11 16:11:42 2006 +0100
+++ b/src/Pure/Isar/isar_syn.ML	Sat Nov 11 16:11:43 2006 +0100
@@ -21,13 +21,6 @@
   OuterSyntax.command "end" "end (local) theory" (K.tag_theory K.thy_end)
     (Scan.succeed (Toplevel.exit o Toplevel.end_local_theory));
 
-val contextP =
-  OuterSyntax.improper_command "context" "switch (local) theory context"
-    (K.tag_theory K.thy_switch)
-    (P.name --| P.begin >> (fn name =>
-      Toplevel.print o IsarThy.context name o
-      Toplevel.begin_local_theory true (TheoryTarget.init (SOME name))));
-
 
 (** markup commands **)
 
@@ -345,6 +338,14 @@
       -- P.text >> (Toplevel.theory o PureThy.add_oracle o P.triple1));
 
 
+(* local theories *)
+
+val contextP =
+  OuterSyntax.command "context" "enter local theory context" K.thy_decl
+    (P.name --| P.begin >> (fn name =>
+      Toplevel.print o Toplevel.begin_local_theory true (TheoryTarget.init (SOME name))));
+
+
 (* locales *)
 
 val locale_val =
@@ -896,7 +897,7 @@
 
 val _ = OuterSyntax.add_parsers [
   (*theory structure*)
-  theoryP, endP, contextP,
+  theoryP, endP,
   (*markup commands*)
   headerP, chapterP, sectionP, subsectionP, subsubsectionP, textP,
   text_rawP, sectP, subsectP, subsubsectP, txtP, txt_rawP,
@@ -909,7 +910,7 @@
   ml_commandP, ml_setupP, setupP, method_setupP,
   parse_ast_translationP, parse_translationP, print_translationP,
   typed_print_translationP, print_ast_translationP,
-  token_translationP, oracleP, localeP,
+  token_translationP, oracleP, contextP, localeP,
   (*proof commands*)
   theoremP, lemmaP, corollaryP, haveP, henceP, showP, thusP, fixP,
   assumeP, presumeP, defP, obtainP, guessP, letP, caseP, thenP, fromP,