--- 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,