src/HOLCF/Tools/domain/domain_axioms.ML
changeset 30919 dcf8a7a66bd1
parent 30912 4022298c1a86
child 31023 d027411c9a38
--- a/src/HOLCF/Tools/domain/domain_axioms.ML	Tue Apr 21 11:11:04 2009 -0700
+++ b/src/HOLCF/Tools/domain/domain_axioms.ML	Tue Apr 21 15:57:08 2009 -0700
@@ -4,7 +4,14 @@
 Syntax generator for domain command.
 *)
 
-structure Domain_Axioms = struct
+signature DOMAIN_AXIOMS =
+sig
+  val add_axioms : bstring -> Domain_Library.eq list -> theory -> theory
+end;
+
+
+structure Domain_Axioms : DOMAIN_AXIOMS =
+struct
 
 local
 
@@ -139,7 +146,7 @@
 
 in (* local *)
 
-fun add_axioms (comp_dnam, eqs : eq list) thy' = let
+fun add_axioms comp_dnam (eqs : eq list) thy' = let
   val comp_dname = Sign.full_bname thy' comp_dnam;
   val dnames = map (fst o fst) eqs;
   val x_name = idx_name dnames "x";