# HG changeset patch
# User huffman
# Date 1288107412 25200
# Node ID 6ba118594692678dcccb137a05138ffb68441dde
# Parent  b63e966564da4ff496c8ca97c65295e8d674fa7e
use Term.add_tfreesT

diff -r b63e966564da -r 6ba118594692 src/HOLCF/Tools/Domain/domain_constructors.ML
--- a/src/HOLCF/Tools/Domain/domain_constructors.ML	Sun Oct 24 15:42:57 2010 -0700
+++ b/src/HOLCF/Tools/Domain/domain_constructors.ML	Tue Oct 26 08:36:52 2010 -0700
@@ -402,7 +402,7 @@
     val abs_inverse = iso_locale RS @{thm iso.abs_iso};
 
     (* calculate function arguments of case combinator *)
-    val tns = map (fst o dest_TFree) (snd (dest_Type lhsT));
+    val tns = map fst (Term.add_tfreesT lhsT []);
     val resultT = TFree (Name.variant tns "'t", @{sort pcpo});
     fun fTs T = map (fn (_, args) => map snd args -->> T) spec;
     val fns = Datatype_Prop.indexify_names (map (K "f") spec);
@@ -770,7 +770,7 @@
     (* get a fresh type variable for the result type *)
     val resultT : typ =
       let
-        val ts : string list = map (fst o dest_TFree) (snd (dest_Type lhsT));
+        val ts : string list = map fst (Term.add_tfreesT lhsT []);
         val t : string = Name.variant ts "'t";
       in TFree (t, @{sort pcpo}) end;