switch to transparent ascription, to avoid warning messages
authorhuffman
Sun Dec 19 18:15:21 2010 -0800 (2010-12-19)
changeset 412966aaf80ea9715
parent 41295 5b5388d4ccc9
child 41297 01b2de947cff
switch to transparent ascription, to avoid warning messages
src/HOL/HOLCF/Tools/Domain/domain.ML
src/HOL/HOLCF/Tools/Domain/domain_constructors.ML
src/HOL/HOLCF/Tools/Domain/domain_induction.ML
src/HOL/HOLCF/Tools/cont_proc.ML
src/HOL/HOLCF/Tools/cpodef.ML
src/HOL/HOLCF/Tools/domaindef.ML
src/HOL/HOLCF/Tools/fixrec.ML
     1.1 --- a/src/HOL/HOLCF/Tools/Domain/domain.ML	Sun Dec 19 18:11:20 2010 -0800
     1.2 +++ b/src/HOL/HOLCF/Tools/Domain/domain.ML	Sun Dec 19 18:15:21 2010 -0800
     1.3 @@ -28,7 +28,7 @@
     1.4        -> theory -> theory
     1.5  end
     1.6  
     1.7 -structure Domain :> DOMAIN =
     1.8 +structure Domain : DOMAIN =
     1.9  struct
    1.10  
    1.11  open HOLCF_Library
     2.1 --- a/src/HOL/HOLCF/Tools/Domain/domain_constructors.ML	Sun Dec 19 18:11:20 2010 -0800
     2.2 +++ b/src/HOL/HOLCF/Tools/Domain/domain_constructors.ML	Sun Dec 19 18:15:21 2010 -0800
     2.3 @@ -34,7 +34,7 @@
     2.4  end
     2.5  
     2.6  
     2.7 -structure Domain_Constructors :> DOMAIN_CONSTRUCTORS =
     2.8 +structure Domain_Constructors : DOMAIN_CONSTRUCTORS =
     2.9  struct
    2.10  
    2.11  open HOLCF_Library
     3.1 --- a/src/HOL/HOLCF/Tools/Domain/domain_induction.ML	Sun Dec 19 18:11:20 2010 -0800
     3.2 +++ b/src/HOL/HOLCF/Tools/Domain/domain_induction.ML	Sun Dec 19 18:15:21 2010 -0800
     3.3 @@ -17,7 +17,7 @@
     3.4    val trace_domain: bool Unsynchronized.ref
     3.5  end
     3.6  
     3.7 -structure Domain_Induction :> DOMAIN_INDUCTION =
     3.8 +structure Domain_Induction : DOMAIN_INDUCTION =
     3.9  struct
    3.10  
    3.11  val quiet_mode = Unsynchronized.ref false
     4.1 --- a/src/HOL/HOLCF/Tools/cont_proc.ML	Sun Dec 19 18:11:20 2010 -0800
     4.2 +++ b/src/HOL/HOLCF/Tools/cont_proc.ML	Sun Dec 19 18:15:21 2010 -0800
     4.3 @@ -12,7 +12,7 @@
     4.4    val setup: theory -> theory
     4.5  end
     4.6  
     4.7 -structure ContProc :> CONT_PROC =
     4.8 +structure ContProc : CONT_PROC =
     4.9  struct
    4.10  
    4.11  (** theory context references **)
     5.1 --- a/src/HOL/HOLCF/Tools/cpodef.ML	Sun Dec 19 18:11:20 2010 -0800
     5.2 +++ b/src/HOL/HOLCF/Tools/cpodef.ML	Sun Dec 19 18:15:21 2010 -0800
     5.3 @@ -38,7 +38,7 @@
     5.4      * (binding * binding) option -> theory -> Proof.state
     5.5  end
     5.6  
     5.7 -structure Cpodef :> CPODEF =
     5.8 +structure Cpodef : CPODEF =
     5.9  struct
    5.10  
    5.11  (** type definitions **)
     6.1 --- a/src/HOL/HOLCF/Tools/domaindef.ML	Sun Dec 19 18:11:20 2010 -0800
     6.2 +++ b/src/HOL/HOLCF/Tools/domaindef.ML	Sun Dec 19 18:15:21 2010 -0800
     6.3 @@ -25,7 +25,7 @@
     6.4      * (binding * binding) option -> theory -> theory
     6.5  end
     6.6  
     6.7 -structure Domaindef :> DOMAINDEF =
     6.8 +structure Domaindef : DOMAINDEF =
     6.9  struct
    6.10  
    6.11  open HOLCF_Library
     7.1 --- a/src/HOL/HOLCF/Tools/fixrec.ML	Sun Dec 19 18:11:20 2010 -0800
     7.2 +++ b/src/HOL/HOLCF/Tools/fixrec.ML	Sun Dec 19 18:15:21 2010 -0800
     7.3 @@ -15,7 +15,7 @@
     7.4    val setup: theory -> theory
     7.5  end
     7.6  
     7.7 -structure Fixrec :> FIXREC =
     7.8 +structure Fixrec : FIXREC =
     7.9  struct
    7.10  
    7.11  open HOLCF_Library