# HG changeset patch
# User huffman
# Date 1289320896 28800
# Node ID 05be0c37db1d72b8baf667f484cd945c06710caf
# Parent  0f37a553bc1a2ace9c6bc130fd9b8ee00af36fa2
add bifiniteness check for domain_isomorphism command

diff -r 0f37a553bc1a -r 05be0c37db1d src/HOLCF/Tools/Domain/domain_isomorphism.ML
--- a/src/HOLCF/Tools/Domain/domain_isomorphism.ML	Tue Nov 09 05:23:34 2010 -0800
+++ b/src/HOLCF/Tools/Domain/domain_isomorphism.ML	Tue Nov 09 08:41:36 2010 -0800
@@ -407,7 +407,7 @@
     (* lookup function for sorts of type variables *)
     fun the_sort v = the (AList.lookup (op =) sorts v);
 
-    (* temporary arities for rewriting *)
+    (* declare arities in temporary theory *)
     val tmp_thy =
       let
         fun arity (vs, tbind, mx, _, _) =
@@ -416,6 +416,13 @@
         fold AxClass.axiomatize_arity (map arity doms) tmp_thy
       end;
 
+    (* check bifiniteness of right-hand sides *)
+    fun check_rhs (vs, tbind, mx, rhs, morphs) =
+      if Sign.of_sort tmp_thy (rhs, @{sort bifinite}) then ()
+      else error ("Type not of sort bifinite: " ^
+        quote (Syntax.string_of_typ_global tmp_thy rhs));
+    val _ = map check_rhs doms;
+
     (* domain equations *)
     fun mk_dom_eqn (vs, tbind, mx, rhs, morphs) =
       let fun arg v = TFree (v, the_sort v);