# HG changeset patch
# User wenzelm
# Date 1113670608 -7200
# Node ID e26fdd4aa95a6d50c08194bcb4350ee36df322a1
# Parent  00d637286a694c649bc487854bf39fae660d478e
added 'no_syntax' command;

diff -r 00d637286a69 -r e26fdd4aa95a src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Sat Apr 16 18:56:37 2005 +0200
+++ b/src/Pure/Isar/isar_syn.ML	Sat Apr 16 18:56:48 2005 +0200
@@ -147,6 +147,10 @@
   OuterSyntax.command "syntax" "declare syntactic constants" K.thy_decl
     (opt_mode -- Scan.repeat1 P.const >> (Toplevel.theory o uncurry Theory.add_modesyntax));
 
+val no_syntaxP =
+  OuterSyntax.command "no_syntax" "delete syntax declarations" K.thy_decl
+    (opt_mode -- Scan.repeat1 P.const >> (Toplevel.theory o uncurry Theory.del_modesyntax));
+
 
 (* translations *)
 
@@ -791,10 +795,10 @@
   text_rawP, sectP, subsectP, subsubsectP, txtP, txt_rawP,
   (*theory sections*)
   classesP, classrelP, defaultsortP, typedeclP, typeabbrP, nontermP,
-  aritiesP, judgmentP, constsP, finalconstsP, syntaxP, translationsP,
-  axiomsP, defsP, constdefsP, theoremsP, lemmasP, declareP, globalP,
-  localP, hideP, useP, mlP, ml_commandP, ml_setupP, setupP,
-  method_setupP, parse_ast_translationP, parse_translationP,
+  aritiesP, judgmentP, constsP, finalconstsP, syntaxP, no_syntaxP,
+  translationsP, axiomsP, defsP, constdefsP, theoremsP, lemmasP,
+  declareP, globalP, localP, hideP, useP, mlP, ml_commandP, ml_setupP,
+  setupP, method_setupP, parse_ast_translationP, parse_translationP,
   print_translationP, typed_print_translationP,
   print_ast_translationP, token_translationP, oracleP, localeP,
   (*proof commands*)