made SML/NJ happy;
authorwenzelm
Tue Sep 02 23:52:51 2008 +0200 (2008-09-02)
changeset 281010bda6ea71615
parent 28100 7650d5e0f8fb
child 28102 d27ea294fdd3
made SML/NJ happy;
src/HOL/Tools/inductive_package.ML
     1.1 --- a/src/HOL/Tools/inductive_package.ML	Tue Sep 02 23:27:44 2008 +0200
     1.2 +++ b/src/HOL/Tools/inductive_package.ML	Tue Sep 02 23:52:51 2008 +0200
     1.3 @@ -727,8 +727,7 @@
     1.4    term list -> (Name.binding * mixfix) list ->
     1.5    local_theory -> inductive_result * local_theory
     1.6  
     1.7 -fun (add_ind_def: add_ind_def)
     1.8 -    {quiet_mode, verbose, kind, alt_name, coind, no_elim, no_ind, skip_mono}
     1.9 +fun add_ind_def {quiet_mode, verbose, kind, alt_name, coind, no_elim, no_ind, skip_mono}
    1.10      cs intros monos params cnames_syn ctxt =
    1.11    let
    1.12      val _ = null cnames_syn andalso error "No inductive predicates given";