src/HOL/Tools/typedef_package.ML
changeset 20462 0cb88ed29776
parent 20357 5fb92bd3aaea
child 20483 04aa552a83bc
--- a/src/HOL/Tools/typedef_package.ML	Fri Sep 01 23:04:42 2006 +0200
+++ b/src/HOL/Tools/typedef_package.ML	Fri Sep 01 23:18:01 2006 +0200
@@ -24,7 +24,6 @@
   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 =