changeset 28084 | a05ca48ef263 |
parent 28083 | 103d9282a946 |
child 28965 | 1de908189869 |
--- a/src/HOL/Tools/function_package/inductive_wrap.ML Tue Sep 02 14:10:45 2008 +0200 +++ b/src/HOL/Tools/function_package/inductive_wrap.ML Tue Sep 02 16:55:33 2008 +0200 @@ -51,7 +51,7 @@ skip_mono = true} [((Name.binding R, T), NoSyn)] (* the relation *) [] (* no parameters *) - (map (fn t => ((Name.no_binding, []), t)) defs) (* the intros *) + (map (fn t => (Attrib.no_binding, t)) defs) (* the intros *) [] (* no special monos *) lthy