signature: do not export private stuff;
authorwenzelm
Fri, 01 Sep 2006 23:18:01 +0200
changeset 20462 0cb88ed29776
parent 20461 d689ad772b2c
child 20463 062c4e9bf3bb
signature: do not export private stuff;
src/HOL/Tools/typedef_package.ML
--- 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 =