# HG changeset patch
# User huffman
# Date 1288108807 25200
# Node ID d8fd7ae0254fa758bf79ee3cbe57610556b201c7
# Parent  6ba118594692678dcccb137a05138ffb68441dde
change types of ML commands add_domain, add_new_domain to take 'sort' instead of 'string option'

diff -r 6ba118594692 -r d8fd7ae0254f src/HOLCF/Tools/Domain/domain.ML
--- a/src/HOLCF/Tools/Domain/domain.ML	Tue Oct 26 08:36:52 2010 -0700
+++ b/src/HOLCF/Tools/Domain/domain.ML	Tue Oct 26 09:00:07 2010 -0700
@@ -13,7 +13,7 @@
       -> theory -> theory
 
   val add_domain:
-      ((string * string option) list * binding * mixfix *
+      ((string * sort) list * binding * mixfix *
        (binding * (bool * binding option * typ) list * mixfix) list) list
       -> theory -> theory
 
@@ -23,7 +23,7 @@
       -> theory -> theory
 
   val add_new_domain:
-      ((string * string option) list * binding * mixfix *
+      ((string * sort) list * binding * mixfix *
        (binding * (bool * binding option * typ) list * mixfix) list) list
       -> theory -> theory
 end;
@@ -43,21 +43,20 @@
      Domain_Take_Proofs.iso_info list * Domain_Take_Proofs.take_induct_info;
 
 fun gen_add_domain
-    (prep_typ : theory -> (string * sort) list -> 'a -> typ)
+    (prep_sort : theory -> 'a -> sort)
+    (prep_typ : theory -> (string * sort) list -> 'b -> typ)
     (add_isos : (binding * mixfix * (typ * typ)) list -> theory -> info * theory)
     (arg_sort : bool -> sort)
-    (raw_specs : ((string * string option) list * binding * mixfix *
-               (binding * (bool * binding option * 'a) list * mixfix) list) list)
+    (raw_specs : ((string * 'a) list * binding * mixfix *
+               (binding * (bool * binding option * 'b) list * mixfix) list) list)
     (thy : theory) =
   let
     val dtnvs : (binding * typ list * mixfix) list =
       let
-        fun readS (SOME s) = Syntax.read_sort_global thy s
-          | readS NONE = Sign.defaultS thy;
-        fun readTFree (a, s) = TFree (a, readS s);
+        fun prep_tvar (a, s) = TFree (a, prep_sort thy s);
       in
         map (fn (vs, dbind, mx, _) =>
-                (dbind, map readTFree vs, mx)) raw_specs
+                (dbind, map prep_tvar vs, mx)) raw_specs
       end;
 
     fun thy_type (dbind, tvars, mx) = (dbind, length tvars, mx);
@@ -73,7 +72,7 @@
     val dbinds : binding list =
         map (fn (_,dbind,_,_) => dbind) raw_specs;
     val raw_rhss :
-        (binding * (bool * binding option * 'a) list * mixfix) list list =
+        (binding * (bool * binding option * 'b) list * mixfix) list list =
         map (fn (_,_,_,cons) => cons) raw_specs;
     val dtnvs' : (string * typ list) list =
         map (fn (dbind, vs, mx) => (Sign.full_name thy dbind, vs)) dtnvs;
@@ -185,6 +184,9 @@
 fun pcpo_arg lazy = if lazy then @{sort cpo} else @{sort pcpo};
 fun rep_arg lazy = @{sort bifinite};
 
+fun read_sort thy (SOME s) = Syntax.read_sort_global thy s
+  | read_sort thy NONE = Sign.defaultS thy;
+
 (* Adapted from src/HOL/Tools/Datatype/datatype_data.ML *)
 fun read_typ thy sorts str =
   let
@@ -204,16 +206,16 @@
   in T end;
 
 val add_domain =
-    gen_add_domain cert_typ Domain_Axioms.add_axioms pcpo_arg;
+    gen_add_domain (K I) cert_typ Domain_Axioms.add_axioms pcpo_arg;
 
 val add_new_domain =
-    gen_add_domain cert_typ define_isos rep_arg;
+    gen_add_domain (K I) cert_typ define_isos rep_arg;
 
 val add_domain_cmd =
-    gen_add_domain read_typ Domain_Axioms.add_axioms pcpo_arg;
+    gen_add_domain read_sort read_typ Domain_Axioms.add_axioms pcpo_arg;
 
 val add_new_domain_cmd =
-    gen_add_domain read_typ define_isos rep_arg;
+    gen_add_domain read_sort read_typ define_isos rep_arg;
 
 
 (** outer syntax **)