# HG changeset patch
# User huffman
# Date 1241037389 25200
# Node ID d027411c9a3812da07164750fd59d83b9b130926
# Parent  a438b4516dd3de4573dff4bbb1692c912d6fa71e
use opaque ascription for all HOLCF code

diff -r a438b4516dd3 -r d027411c9a38 src/HOLCF/Tools/adm_tac.ML
--- a/src/HOLCF/Tools/adm_tac.ML	Wed Apr 29 21:10:46 2009 +0200
+++ b/src/HOLCF/Tools/adm_tac.ML	Wed Apr 29 13:36:29 2009 -0700
@@ -18,7 +18,7 @@
   val adm_tac: Proof.context -> (int -> tactic) -> int -> tactic
 end;
 
-structure Adm: ADM =
+structure Adm :> ADM =
 struct
 
 
diff -r a438b4516dd3 -r d027411c9a38 src/HOLCF/Tools/cont_consts.ML
--- a/src/HOLCF/Tools/cont_consts.ML	Wed Apr 29 21:10:46 2009 +0200
+++ b/src/HOLCF/Tools/cont_consts.ML	Wed Apr 29 13:36:29 2009 -0700
@@ -12,7 +12,7 @@
   val add_consts_i: (binding * typ * mixfix) list -> theory -> theory
 end;
 
-structure ContConsts: CONT_CONSTS =
+structure ContConsts :> CONT_CONSTS =
 struct
 
 
diff -r a438b4516dd3 -r d027411c9a38 src/HOLCF/Tools/cont_proc.ML
--- a/src/HOLCF/Tools/cont_proc.ML	Wed Apr 29 21:10:46 2009 +0200
+++ b/src/HOLCF/Tools/cont_proc.ML	Wed Apr 29 13:36:29 2009 -0700
@@ -12,7 +12,7 @@
   val setup: theory -> theory
 end;
 
-structure ContProc: CONT_PROC =
+structure ContProc :> CONT_PROC =
 struct
 
 (** theory context references **)
diff -r a438b4516dd3 -r d027411c9a38 src/HOLCF/Tools/domain/domain_axioms.ML
--- a/src/HOLCF/Tools/domain/domain_axioms.ML	Wed Apr 29 21:10:46 2009 +0200
+++ b/src/HOLCF/Tools/domain/domain_axioms.ML	Wed Apr 29 13:36:29 2009 -0700
@@ -10,7 +10,7 @@
 end;
 
 
-structure Domain_Axioms : DOMAIN_AXIOMS =
+structure Domain_Axioms :> DOMAIN_AXIOMS =
 struct
 
 local
diff -r a438b4516dd3 -r d027411c9a38 src/HOLCF/Tools/domain/domain_extender.ML
--- a/src/HOLCF/Tools/domain/domain_extender.ML	Wed Apr 29 21:10:46 2009 +0200
+++ b/src/HOLCF/Tools/domain/domain_extender.ML	Wed Apr 29 13:36:29 2009 -0700
@@ -14,7 +14,7 @@
     -> theory -> theory
 end;
 
-structure Domain_Extender: DOMAIN_EXTENDER =
+structure Domain_Extender :> DOMAIN_EXTENDER =
 struct
 
 open Domain_Library;
diff -r a438b4516dd3 -r d027411c9a38 src/HOLCF/Tools/domain/domain_library.ML
--- a/src/HOLCF/Tools/domain/domain_library.ML	Wed Apr 29 21:10:46 2009 +0200
+++ b/src/HOLCF/Tools/domain/domain_library.ML	Wed Apr 29 13:36:29 2009 -0700
@@ -151,7 +151,7 @@
   val mk_var_names : string list -> string list;
 end;
 
-structure Domain_Library : DOMAIN_LIBRARY =
+structure Domain_Library :> DOMAIN_LIBRARY =
 struct
 
 exception Impossible of string;
diff -r a438b4516dd3 -r d027411c9a38 src/HOLCF/Tools/domain/domain_syntax.ML
--- a/src/HOLCF/Tools/domain/domain_syntax.ML	Wed Apr 29 21:10:46 2009 +0200
+++ b/src/HOLCF/Tools/domain/domain_syntax.ML	Wed Apr 29 13:36:29 2009 -0700
@@ -12,7 +12,7 @@
 end;
 
 
-structure Domain_Syntax : DOMAIN_SYNTAX =
+structure Domain_Syntax :> DOMAIN_SYNTAX =
 struct 
 
 local 
diff -r a438b4516dd3 -r d027411c9a38 src/HOLCF/Tools/domain/domain_theorems.ML
--- a/src/HOLCF/Tools/domain/domain_theorems.ML	Wed Apr 29 21:10:46 2009 +0200
+++ b/src/HOLCF/Tools/domain/domain_theorems.ML	Wed Apr 29 13:36:29 2009 -0700
@@ -14,7 +14,7 @@
   val comp_theorems: bstring * Domain_Library.eq list -> theory -> thm list * theory;
 end;
 
-structure Domain_Theorems : DOMAIN_THEOREMS =
+structure Domain_Theorems :> DOMAIN_THEOREMS =
 struct
 
 val quiet_mode = ref false;
diff -r a438b4516dd3 -r d027411c9a38 src/HOLCF/Tools/fixrec_package.ML
--- a/src/HOLCF/Tools/fixrec_package.ML	Wed Apr 29 21:10:46 2009 +0200
+++ b/src/HOLCF/Tools/fixrec_package.ML	Wed Apr 29 13:36:29 2009 -0700
@@ -16,7 +16,7 @@
   val setup: theory -> theory
 end;
 
-structure FixrecPackage: FIXREC_PACKAGE =
+structure FixrecPackage :> FIXREC_PACKAGE =
 struct
 
 val fix_eq2 = @{thm fix_eq2};
diff -r a438b4516dd3 -r d027411c9a38 src/HOLCF/Tools/pcpodef_package.ML
--- a/src/HOLCF/Tools/pcpodef_package.ML	Wed Apr 29 21:10:46 2009 +0200
+++ b/src/HOLCF/Tools/pcpodef_package.ML	Wed Apr 29 13:36:29 2009 -0700
@@ -17,7 +17,7 @@
     * (binding * binding) option -> theory -> Proof.state
 end;
 
-structure PcpodefPackage: PCPODEF_PACKAGE =
+structure PcpodefPackage :> PCPODEF_PACKAGE =
 struct
 
 (** type definitions **)