--- a/src/HOL/Tools/inductive_codegen.ML Tue Jul 14 10:53:44 2009 +0200
+++ b/src/HOL/Tools/inductive_codegen.ML Tue Jul 14 10:54:04 2009 +0200
@@ -697,7 +697,8 @@
val setup =
add_codegen "inductive" inductive_codegen #>
- Code.add_attribute ("ind", Scan.option (Args.$$$ "target" |-- Args.colon |-- Args.name) --
- Scan.option (Args.$$$ "params" |-- Args.colon |-- OuterParse.nat) >> uncurry add);
+ Attrib.setup @{binding code_ind} (Scan.lift (Scan.option (Args.$$$ "target" |-- Args.colon |-- Args.name) --
+ Scan.option (Args.$$$ "params" |-- Args.colon |-- OuterParse.nat) >> uncurry add))
+ "introduction rules for executable predicates";
end;