1.1 --- a/src/HOLCF/Tools/adm_tac.ML	Wed Apr 29 21:10:46 2009 +0200
     1.2 +++ b/src/HOLCF/Tools/adm_tac.ML	Wed Apr 29 13:36:29 2009 -0700
     1.3 @@ -18,7 +18,7 @@
     1.4    val adm_tac: Proof.context -> (int -> tactic) -> int -> tactic
     1.5  end;
     1.6  
     1.7 -structure Adm: ADM =
     1.8 +structure Adm :> ADM =
     1.9  struct
    1.10  
    1.11  

     2.1 --- a/src/HOLCF/Tools/cont_consts.ML	Wed Apr 29 21:10:46 2009 +0200
     2.2 +++ b/src/HOLCF/Tools/cont_consts.ML	Wed Apr 29 13:36:29 2009 -0700
     2.3 @@ -12,7 +12,7 @@
     2.4    val add_consts_i: (binding * typ * mixfix) list -> theory -> theory
     2.5  end;
     2.6  
     2.7 -structure ContConsts: CONT_CONSTS =
     2.8 +structure ContConsts :> CONT_CONSTS =
     2.9  struct
    2.10  
    2.11  

     3.1 --- a/src/HOLCF/Tools/cont_proc.ML	Wed Apr 29 21:10:46 2009 +0200
     3.2 +++ b/src/HOLCF/Tools/cont_proc.ML	Wed Apr 29 13:36:29 2009 -0700
     3.3 @@ -12,7 +12,7 @@
     3.4    val setup: theory -> theory
     3.5  end;
     3.6  
     3.7 -structure ContProc: CONT_PROC =
     3.8 +structure ContProc :> CONT_PROC =
     3.9  struct
    3.10  
    3.11  (** theory context references **)

     4.1 --- a/src/HOLCF/Tools/domain/domain_axioms.ML	Wed Apr 29 21:10:46 2009 +0200
     4.2 +++ b/src/HOLCF/Tools/domain/domain_axioms.ML	Wed Apr 29 13:36:29 2009 -0700
     4.3 @@ -10,7 +10,7 @@
     4.4  end;
     4.5  
     4.6  
     4.7 -structure Domain_Axioms : DOMAIN_AXIOMS =
     4.8 +structure Domain_Axioms :> DOMAIN_AXIOMS =
     4.9  struct
    4.10  
    4.11  local

     5.1 --- a/src/HOLCF/Tools/domain/domain_extender.ML	Wed Apr 29 21:10:46 2009 +0200
     5.2 +++ b/src/HOLCF/Tools/domain/domain_extender.ML	Wed Apr 29 13:36:29 2009 -0700
     5.3 @@ -14,7 +14,7 @@
     5.4      -> theory -> theory
     5.5  end;
     5.6  
     5.7 -structure Domain_Extender: DOMAIN_EXTENDER =
     5.8 +structure Domain_Extender :> DOMAIN_EXTENDER =
     5.9  struct
    5.10  
    5.11  open Domain_Library;

     6.1 --- a/src/HOLCF/Tools/domain/domain_library.ML	Wed Apr 29 21:10:46 2009 +0200
     6.2 +++ b/src/HOLCF/Tools/domain/domain_library.ML	Wed Apr 29 13:36:29 2009 -0700
     6.3 @@ -151,7 +151,7 @@
     6.4    val mk_var_names : string list -> string list;
     6.5  end;
     6.6  
     6.7 -structure Domain_Library : DOMAIN_LIBRARY =
     6.8 +structure Domain_Library :> DOMAIN_LIBRARY =
     6.9  struct
    6.10  
    6.11  exception Impossible of string;

     7.1 --- a/src/HOLCF/Tools/domain/domain_syntax.ML	Wed Apr 29 21:10:46 2009 +0200
     7.2 +++ b/src/HOLCF/Tools/domain/domain_syntax.ML	Wed Apr 29 13:36:29 2009 -0700
     7.3 @@ -12,7 +12,7 @@
     7.4  end;
     7.5  
     7.6  
     7.7 -structure Domain_Syntax : DOMAIN_SYNTAX =
     7.8 +structure Domain_Syntax :> DOMAIN_SYNTAX =
     7.9  struct 
    7.10  
    7.11  local 

     8.1 --- a/src/HOLCF/Tools/domain/domain_theorems.ML	Wed Apr 29 21:10:46 2009 +0200
     8.2 +++ b/src/HOLCF/Tools/domain/domain_theorems.ML	Wed Apr 29 13:36:29 2009 -0700
     8.3 @@ -14,7 +14,7 @@
     8.4    val comp_theorems: bstring * Domain_Library.eq list -> theory -> thm list * theory;
     8.5  end;
     8.6  
     8.7 -structure Domain_Theorems : DOMAIN_THEOREMS =
     8.8 +structure Domain_Theorems :> DOMAIN_THEOREMS =
     8.9  struct
    8.10  
    8.11  val quiet_mode = ref false;

     9.1 --- a/src/HOLCF/Tools/fixrec_package.ML	Wed Apr 29 21:10:46 2009 +0200
     9.2 +++ b/src/HOLCF/Tools/fixrec_package.ML	Wed Apr 29 13:36:29 2009 -0700
     9.3 @@ -16,7 +16,7 @@
     9.4    val setup: theory -> theory
     9.5  end;
     9.6  
     9.7 -structure FixrecPackage: FIXREC_PACKAGE =
     9.8 +structure FixrecPackage :> FIXREC_PACKAGE =
     9.9  struct
    9.10  
    9.11  val fix_eq2 = @{thm fix_eq2};

    10.1 --- a/src/HOLCF/Tools/pcpodef_package.ML	Wed Apr 29 21:10:46 2009 +0200
    10.2 +++ b/src/HOLCF/Tools/pcpodef_package.ML	Wed Apr 29 13:36:29 2009 -0700
    10.3 @@ -17,7 +17,7 @@
    10.4      * (binding * binding) option -> theory -> Proof.state
    10.5  end;
    10.6  
    10.7 -structure PcpodefPackage: PCPODEF_PACKAGE =
    10.8 +structure PcpodefPackage :> PCPODEF_PACKAGE =
    10.9  struct
   10.10  
   10.11  (** type definitions **)