--- a/src/HOL/Tools/inductive_set.ML Sun Jul 31 11:13:38 2011 -0700
+++ b/src/HOL/Tools/inductive_set.ML Mon Aug 01 12:08:53 2011 +0200
@@ -524,7 +524,7 @@
Inductive.declare_rules rec_name coind no_ind cnames (map fst defs)
(map (to_set [] (Context.Proof lthy3)) intrs) intr_names intr_atts
(map (fn th => (to_set [] (Context.Proof lthy3) th,
- map fst (fst (Rule_Cases.get th)),
+ map (fst o fst) (fst (Rule_Cases.get th)),
Rule_Cases.get_constraints th)) elims)
(map (to_set [] (Context.Proof lthy3)) eqs) raw_induct' lthy3;
in