src/HOL/Tools/datatype_codegen.ML
changeset 22296 c9e7c6e73de3
parent 22175 d9e3e4c30d6b
child 22331 7df6bc8cf0b0
--- 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