src/HOLCF/Tools/Domain/domain_syntax.ML

--- a/src/HOLCF/Tools/Domain/domain_syntax.ML	Tue Mar 02 14:41:16 2010 -0800
+++ b/src/HOLCF/Tools/Domain/domain_syntax.ML	Tue Mar 02 14:59:24 2010 -0800
@@ -8,13 +8,11 @@
 sig
   val calc_syntax:
       theory ->
-      bool ->
       (string * typ list) *
       (binding * (bool * binding option * typ) list * mixfix) list ->
       (binding * typ * mixfix) list
 
   val add_syntax:
-      bool ->
       ((string * typ list) *
        (binding * (bool * binding option * typ) list * mixfix) list) list ->
       theory -> theory
@@ -28,7 +26,6 @@
 infixr 5 -->; infixr 6 ->>;
 
 fun calc_syntax thy
-    (definitional : bool)
     ((dname : string, typevars : typ list), 
      (cons': (binding * (bool * binding option * typ) list * mixfix) list))
     : (binding * typ * mixfix) list =
@@ -47,24 +44,19 @@
     val const_abs  = (dbind "_abs" ,              dtype2 ->> dtype , NoSyn);
     end;
 
-    val optional_consts =
-        if definitional then [] else [const_rep, const_abs];
-
-  in optional_consts
-  end; (* let *)
+  in [const_rep, const_abs] end;
 
 (* ----- putting all the syntax stuff together ------------------------------ *)
 
 fun add_syntax
-    (definitional : bool)
     (eqs' : ((string * typ list) *
              (binding * (bool * binding option * typ) list * mixfix) list) list)
-    (thy'' : theory) =
+    (thy : theory) =
   let
     val ctt : (binding * typ * mixfix) list list =
-        map (calc_syntax thy'' definitional) eqs';
-  in thy''
-       |> Cont_Consts.add_consts (flat ctt)
-  end; (* let *)
+        map (calc_syntax thy) eqs';
+  in
+    Cont_Consts.add_consts (flat ctt) thy
+  end;
 
 end; (* struct *)