src/HOL/HOLCF/Tools/Domain/domain_induction.ML
changeset 41296 6aaf80ea9715
parent 41214 8a341cf54a85
child 42151 4da4fc77664b
     1.1 --- a/src/HOL/HOLCF/Tools/Domain/domain_induction.ML	Sun Dec 19 18:11:20 2010 -0800
     1.2 +++ b/src/HOL/HOLCF/Tools/Domain/domain_induction.ML	Sun Dec 19 18:15:21 2010 -0800
     1.3 @@ -17,7 +17,7 @@
     1.4    val trace_domain: bool Unsynchronized.ref
     1.5  end
     1.6  
     1.7 -structure Domain_Induction :> DOMAIN_INDUCTION =
     1.8 +structure Domain_Induction : DOMAIN_INDUCTION =
     1.9  struct
    1.10  
    1.11  val quiet_mode = Unsynchronized.ref false