# 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;