# HG changeset patch
# User wenzelm
# Date 1142350177 -3600
# Node ID a3d3a4b75c71e76b95774e3da89c68009fbb7784
# Parent  196d3b7c8ad1af0fe1b05c5cb27b710d51d4c5f6
added 'no_translations';

diff -r 196d3b7c8ad1 -r a3d3a4b75c71 src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Tue Mar 14 16:29:36 2006 +0100
+++ b/src/Pure/Isar/isar_syn.ML	Tue Mar 14 16:29:37 2006 +0100
@@ -169,6 +169,10 @@
   OuterSyntax.command "translations" "declare syntax translation rules" K.thy_decl
     (Scan.repeat1 trans_line >> (Toplevel.theory o Theory.add_trrules));
 
+val no_translationsP =
+  OuterSyntax.command "no_translations" "remove syntax translation rules" K.thy_decl
+    (Scan.repeat1 trans_line >> (Toplevel.theory o Theory.del_trrules));
+
 
 (* axioms and definitions *)
 
@@ -875,11 +879,11 @@
   (*theory sections*)
   classesP, classrelP, defaultsortP, axclassP, typedeclP, typeabbrP,
   nontermP, aritiesP, judgmentP, constsP, finalconstsP, syntaxP,
-  no_syntaxP, translationsP, axiomsP, defsP, constdefsP, definitionP,
-  abbreviationP, axiomatizationP, 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,
+  no_syntaxP, translationsP, no_translationsP, axiomsP, defsP,
+  constdefsP, definitionP, abbreviationP, axiomatizationP, 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*)
   theoremP, lemmaP, corollaryP, haveP, henceP, showP, thusP, fixP,