# HG changeset patch
# User wenzelm
# Date 1215703587 -7200
# Node ID 69618a03b6f7e9e92923f3930d3822581109c0e2
# Parent  ee2721e9e900637b00744eaa7a5bfa8d3c672ff3
change_lexicons: no verbosity;

diff -r ee2721e9e900 -r 69618a03b6f7 src/Pure/Isar/outer_keyword.ML
--- a/src/Pure/Isar/outer_keyword.ML	Thu Jul 10 17:26:25 2008 +0200
+++ b/src/Pure/Isar/outer_keyword.ML	Thu Jul 10 17:26:27 2008 +0200
@@ -119,12 +119,7 @@
 fun get_lexicons () = CRITICAL (fn () => ! global_lexicons);
 
 fun change_commands f = CRITICAL (fn () => change global_commands f);
-
-fun change_lexicons f = CRITICAL (fn () =>
-  (change global_lexicons f;
-    (case (op inter_string) (pairself Scan.dest_lexicon (get_lexicons ())) of
-      [] => ()
-    | clash => warning ("Overlapping outer syntax commands and keywords: " ^ commas_quote clash))));
+fun change_lexicons f = CRITICAL (fn () => change global_lexicons f);
 
 end;