# HG changeset patch
# User huffman
# Date 1292811321 28800
# Node ID 6aaf80ea9715ab938518999aaca913809ae439d7
# Parent  5b5388d4ccc930cf38297788eb407be3b8bc525b
switch to transparent ascription, to avoid warning messages

diff -r 5b5388d4ccc9 -r 6aaf80ea9715 src/HOL/HOLCF/Tools/Domain/domain.ML
--- a/src/HOL/HOLCF/Tools/Domain/domain.ML	Sun Dec 19 18:11:20 2010 -0800
+++ b/src/HOL/HOLCF/Tools/Domain/domain.ML	Sun Dec 19 18:15:21 2010 -0800
@@ -28,7 +28,7 @@
       -> theory -> theory
 end
 
-structure Domain :> DOMAIN =
+structure Domain : DOMAIN =
 struct
 
 open HOLCF_Library
diff -r 5b5388d4ccc9 -r 6aaf80ea9715 src/HOL/HOLCF/Tools/Domain/domain_constructors.ML
--- a/src/HOL/HOLCF/Tools/Domain/domain_constructors.ML	Sun Dec 19 18:11:20 2010 -0800
+++ b/src/HOL/HOLCF/Tools/Domain/domain_constructors.ML	Sun Dec 19 18:15:21 2010 -0800
@@ -34,7 +34,7 @@
 end
 
 
-structure Domain_Constructors :> DOMAIN_CONSTRUCTORS =
+structure Domain_Constructors : DOMAIN_CONSTRUCTORS =
 struct
 
 open HOLCF_Library
diff -r 5b5388d4ccc9 -r 6aaf80ea9715 src/HOL/HOLCF/Tools/Domain/domain_induction.ML
--- a/src/HOL/HOLCF/Tools/Domain/domain_induction.ML	Sun Dec 19 18:11:20 2010 -0800
+++ b/src/HOL/HOLCF/Tools/Domain/domain_induction.ML	Sun Dec 19 18:15:21 2010 -0800
@@ -17,7 +17,7 @@
   val trace_domain: bool Unsynchronized.ref
 end
 
-structure Domain_Induction :> DOMAIN_INDUCTION =
+structure Domain_Induction : DOMAIN_INDUCTION =
 struct
 
 val quiet_mode = Unsynchronized.ref false
diff -r 5b5388d4ccc9 -r 6aaf80ea9715 src/HOL/HOLCF/Tools/cont_proc.ML
--- a/src/HOL/HOLCF/Tools/cont_proc.ML	Sun Dec 19 18:11:20 2010 -0800
+++ b/src/HOL/HOLCF/Tools/cont_proc.ML	Sun Dec 19 18:15:21 2010 -0800
@@ -12,7 +12,7 @@
   val setup: theory -> theory
 end
 
-structure ContProc :> CONT_PROC =
+structure ContProc : CONT_PROC =
 struct
 
 (** theory context references **)
diff -r 5b5388d4ccc9 -r 6aaf80ea9715 src/HOL/HOLCF/Tools/cpodef.ML
--- a/src/HOL/HOLCF/Tools/cpodef.ML	Sun Dec 19 18:11:20 2010 -0800
+++ b/src/HOL/HOLCF/Tools/cpodef.ML	Sun Dec 19 18:15:21 2010 -0800
@@ -38,7 +38,7 @@
     * (binding * binding) option -> theory -> Proof.state
 end
 
-structure Cpodef :> CPODEF =
+structure Cpodef : CPODEF =
 struct
 
 (** type definitions **)
diff -r 5b5388d4ccc9 -r 6aaf80ea9715 src/HOL/HOLCF/Tools/domaindef.ML
--- a/src/HOL/HOLCF/Tools/domaindef.ML	Sun Dec 19 18:11:20 2010 -0800
+++ b/src/HOL/HOLCF/Tools/domaindef.ML	Sun Dec 19 18:15:21 2010 -0800
@@ -25,7 +25,7 @@
     * (binding * binding) option -> theory -> theory
 end
 
-structure Domaindef :> DOMAINDEF =
+structure Domaindef : DOMAINDEF =
 struct
 
 open HOLCF_Library
diff -r 5b5388d4ccc9 -r 6aaf80ea9715 src/HOL/HOLCF/Tools/fixrec.ML
--- a/src/HOL/HOLCF/Tools/fixrec.ML	Sun Dec 19 18:11:20 2010 -0800
+++ b/src/HOL/HOLCF/Tools/fixrec.ML	Sun Dec 19 18:15:21 2010 -0800
@@ -15,7 +15,7 @@
   val setup: theory -> theory
 end
 
-structure Fixrec :> FIXREC =
+structure Fixrec : FIXREC =
 struct
 
 open HOLCF_Library