# HG changeset patch
# User huffman
# Date 1267570764 28800
# Node ID 3b20559d809bfab781e746fad25257cfc135f1ac
# Parent  0e2ef13796a475188f64a6072c9f8166c9edf7a9
add_syntax no longer needs a definitional mode

diff -r 0e2ef13796a4 -r 3b20559d809b src/HOLCF/Tools/Domain/domain_extender.ML
--- a/src/HOLCF/Tools/Domain/domain_extender.ML	Tue Mar 02 14:41:16 2010 -0800
+++ b/src/HOLCF/Tools/Domain/domain_extender.ML	Tue Mar 02 14:59:24 2010 -0800
@@ -150,7 +150,7 @@
     val eqs' : ((string * typ list) *
         (binding * (bool * binding option * typ) list * mixfix) list) list =
       check_and_sort_domain false dtnvs' cons'' thy;
-    val thy = thy |> Domain_Syntax.add_syntax false eqs';
+    val thy = Domain_Syntax.add_syntax eqs' thy;
     val dts  = map (Type o fst) eqs';
     val new_dts = map (fn ((s,Ts),_) => (s, map (fst o dest_TFree) Ts)) eqs';
     fun strip ss = drop (find_index (fn s => s = "'") ss + 1) ss;
@@ -223,7 +223,6 @@
                  (map fst vs, dname, mx, mk_eq_typ eq, NONE))
              (eqs''' ~~ eqs'))
 
-    val thy = thy |> Domain_Syntax.add_syntax true eqs';
     val dts  = map (Type o fst) eqs';
     val new_dts = map (fn ((s,Ts),_) => (s, map (fst o dest_TFree) Ts)) eqs';
     fun strip ss = drop (find_index (fn s => s = "'") ss + 1) ss;
diff -r 0e2ef13796a4 -r 3b20559d809b 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 *)