# HG changeset patch
# User wenzelm
# Date 1183917111 -7200
# Node ID 6e0b8b6012c941a91cfd29c47f6cb709744abfac
# Parent  0a6a719d24d58a90ee569d2097610f02474dab79
renamed ML_exc to ML_exn;

diff -r 0a6a719d24d5 -r 6e0b8b6012c9 doc-src/antiquote_setup.ML
--- a/doc-src/antiquote_setup.ML	Sun Jul 08 19:01:32 2007 +0200
+++ b/doc-src/antiquote_setup.ML	Sun Jul 08 19:51:51 2007 +0200
@@ -17,8 +17,8 @@
 fun ml_type (txt1, "") = "val _ = NONE : (" ^ txt1 ^ ") option;"
   | ml_type (txt1, txt2) = "val _ = [NONE : (" ^ txt1 ^ ") option, NONE : (" ^ txt2 ^ ") option];";
 
-fun ml_exc (txt1, "") = "fn _ => (" ^ txt1 ^ ": exn);"
-  | ml_exc (txt1, txt2) = "fn _ => (" ^ txt1 ^ ": " ^ txt2 ^ " -> exn);";
+fun ml_exn (txt1, "") = "fn _ => (" ^ txt1 ^ ": exn);"
+  | ml_exn (txt1, txt2) = "fn _ => (" ^ txt1 ^ ": " ^ txt2 ^ " -> exn);";
 
 fun ml_structure (txt, _) = "functor DUMMY_FUNCTOR() = struct structure DUMMY = " ^ txt ^ " end;"
 
@@ -57,7 +57,7 @@
 val _ = O.add_commands
  [("index_ML", arguments (index_ml "" ml_val)),
   ("index_ML_type", arguments (index_ml "type" ml_type)),
-  ("index_ML_exc", arguments (index_ml "exception" ml_exc)),
+  ("index_ML_exn", arguments (index_ml "exception" ml_exn)),
   ("index_ML_structure", arguments (index_ml "structure" ml_structure)),
   ("index_ML_functor", arguments (index_ml "functor" ml_functor)),
   ("ML_functor", O.args (Scan.lift Args.name) output_verbatim),