# HG changeset patch
# User berghofe
# Date 1064239565 -7200
# Node ID e7c9206dd2ef7ef88088061da509032694de64c9
# Parent  8953b566dfed188613d5d29381d2ae848ff3ee96
Changed interface of add_attribute.

diff -r 8953b566dfed -r e7c9206dd2ef src/HOL/Tools/inductive_codegen.ML
--- a/src/HOL/Tools/inductive_codegen.ML	Mon Sep 22 16:04:49 2003 +0200
+++ b/src/HOL/Tools/inductive_codegen.ML	Mon Sep 22 16:06:05 2003 +0200
@@ -542,7 +542,7 @@
 val setup =
   [add_codegen "inductive" inductive_codegen,
    CodegenData.init,
-   add_attribute "ind" add];
+   add_attribute "ind" (Scan.succeed add)];
 
 end;