# HG changeset patch
# User haftmann
# Date 1171095975 -3600
# Node ID c9e7c6e73de3c574503eb2e9fe04fba3d338bcf4
# Parent  5f8a2898668c1e0542ec13c8eb12d69799162d3f
canonical interface for attributes

diff -r 5f8a2898668c -r c9e7c6e73de3 src/HOL/Tools/datatype_codegen.ML
--- a/src/HOL/Tools/datatype_codegen.ML	Sat Feb 10 09:26:14 2007 +0100
+++ b/src/HOL/Tools/datatype_codegen.ML	Sat Feb 10 09:26:15 2007 +0100
@@ -28,7 +28,7 @@
     -> (string * (((string * sort list) * sort) * term list)) list option
   val prove_codetypes_arities: tactic -> (string * bool) list -> sort
     -> (((string * sort list) * sort) list -> (string * term list) list -> theory
-    -> ((bstring * attribute list) * term) list * theory)
+    -> ((bstring * Attrib.src list) * term) list * theory)
     -> (((string * sort list) * sort) list -> (string * term list) list -> theory -> theory)
     -> theory -> theory