# HG changeset patch
# User haftmann
# Date 1155018024 -7200
# Node ID 5fb92bd3aaeae39bb417813d4cf666841a34e69c
# Parent  21e7e90939408f83f0b0e1d5225e6490487f6cf6
fixed code generator theorem generation

diff -r 21e7e9093940 -r 5fb92bd3aaea src/HOL/Tools/typedef_package.ML
--- a/src/HOL/Tools/typedef_package.ML	Tue Aug 08 08:19:47 2006 +0200
+++ b/src/HOL/Tools/typedef_package.ML	Tue Aug 08 08:20:24 2006 +0200
@@ -24,6 +24,7 @@
   val typedef_i: (bool * string) * (bstring * string list * mixfix) * term
     * (string * string) option -> theory -> Proof.state
   val setup: theory -> theory
+  structure TypedefData: THEORY_DATA
 end;
 
 structure TypedefPackage: TYPEDEF_PACKAGE =