# HG changeset patch
# User wenzelm
# Date 1220392371 -7200
# Node ID 0bda6ea716159b12d45c25d4b32c85ec43e8cedd
# Parent  7650d5e0f8fb89c2a58536abc5df68adad5b4feb
made SML/NJ happy;

diff -r 7650d5e0f8fb -r 0bda6ea71615 src/HOL/Tools/inductive_package.ML
--- a/src/HOL/Tools/inductive_package.ML	Tue Sep 02 23:27:44 2008 +0200
+++ b/src/HOL/Tools/inductive_package.ML	Tue Sep 02 23:52:51 2008 +0200
@@ -727,8 +727,7 @@
   term list -> (Name.binding * mixfix) list ->
   local_theory -> inductive_result * local_theory
 
-fun (add_ind_def: add_ind_def)
-    {quiet_mode, verbose, kind, alt_name, coind, no_elim, no_ind, skip_mono}
+fun add_ind_def {quiet_mode, verbose, kind, alt_name, coind, no_elim, no_ind, skip_mono}
     cs intros monos params cnames_syn ctxt =
   let
     val _ = null cnames_syn andalso error "No inductive predicates given";