diff -r eb8e231a335f -r 154855d9a564 src/Doc/antiquote_setup.ML --- a/src/Doc/antiquote_setup.ML Sun Mar 02 18:41:41 2014 +0100 +++ b/src/Doc/antiquote_setup.ML Sun Mar 02 19:00:45 2014 +0100 @@ -64,8 +64,8 @@ ml_toks "val _ = [NONE : (" @ toks1 @ ml_toks ") option, NONE : (" @ toks2 @ ml_toks ") option];"; -fun ml_exn (toks1, []) = ml_toks "fn _ => (" @ toks1 @ ml_toks " : exn);" - | ml_exn (toks1, toks2) = +fun ml_exception (toks1, []) = ml_toks "fn _ => (" @ toks1 @ ml_toks " : exn);" + | ml_exception (toks1, toks2) = ml_toks "fn _ => (" @ toks1 @ ml_toks " : " @ toks2 @ ml_toks " -> exn);"; fun ml_structure (toks, _) = @@ -121,8 +121,8 @@ index_ml @{binding index_ML} "" ml_val #> index_ml @{binding index_ML_op} "infix" ml_op #> index_ml @{binding index_ML_type} "type" ml_type #> - index_ml @{binding index_ML_exn} "exception" ml_exn #> - index_ml @{binding index_ML_struct} "structure" ml_structure #> + index_ml @{binding index_ML_exception} "exception" ml_exception #> + index_ml @{binding index_ML_structure} "structure" ml_structure #> index_ml @{binding index_ML_functor} "functor" ml_functor; end;