src/Doc/antiquote_setup.ML
changeset 55837 154855d9a564
parent 55831 3a9386b32211
child 55997 9dc5ce83202c
     1.1 --- a/src/Doc/antiquote_setup.ML	Sun Mar 02 18:41:41 2014 +0100
     1.2 +++ b/src/Doc/antiquote_setup.ML	Sun Mar 02 19:00:45 2014 +0100
     1.3 @@ -64,8 +64,8 @@
     1.4        ml_toks "val _ = [NONE : (" @ toks1 @ ml_toks ") option, NONE : (" @
     1.5          toks2 @ ml_toks ") option];";
     1.6  
     1.7 -fun ml_exn (toks1, []) = ml_toks "fn _ => (" @ toks1 @ ml_toks " : exn);"
     1.8 -  | ml_exn (toks1, toks2) =
     1.9 +fun ml_exception (toks1, []) = ml_toks "fn _ => (" @ toks1 @ ml_toks " : exn);"
    1.10 +  | ml_exception (toks1, toks2) =
    1.11        ml_toks "fn _ => (" @ toks1 @ ml_toks " : " @ toks2 @ ml_toks " -> exn);";
    1.12  
    1.13  fun ml_structure (toks, _) =
    1.14 @@ -121,8 +121,8 @@
    1.15    index_ml @{binding index_ML} "" ml_val #>
    1.16    index_ml @{binding index_ML_op} "infix" ml_op #>
    1.17    index_ml @{binding index_ML_type} "type" ml_type #>
    1.18 -  index_ml @{binding index_ML_exn} "exception" ml_exn #>
    1.19 -  index_ml @{binding index_ML_struct} "structure" ml_structure #>
    1.20 +  index_ml @{binding index_ML_exception} "exception" ml_exception #>
    1.21 +  index_ml @{binding index_ML_structure} "structure" ml_structure #>
    1.22    index_ml @{binding index_ML_functor} "functor" ml_functor;
    1.23  
    1.24  end;