--- a/src/HOL/Tools/inductive_set.ML Tue Mar 13 17:17:52 2012 +0000
+++ b/src/HOL/Tools/inductive_set.ML Tue Mar 13 20:04:24 2012 +0100
@@ -498,7 +498,7 @@
val (defs, lthy2) = lthy1
|> Local_Theory.conceal (* FIXME ?? *)
|> fold_map Local_Theory.define
- (map (fn ((c_syn, (fs, U, _)), p) => (c_syn, (Attrib.empty_binding,
+ (map (fn (((c, syn), (fs, U, _)), p) => ((c, syn), ((Thm.def_binding c, []),
fold_rev lambda params (HOLogic.Collect_const U $
HOLogic.mk_psplits fs U HOLogic.boolT (list_comb (p, params3))))))
(cnames_syn ~~ cs_info ~~ preds))