# HG changeset patch
# User huffman
# Date 1267207897 28800
# Node ID 490a6e6c737993540ceb79c0cfda087cabeb97e8
# Parent  cf6ba350b7ca730ff556dd1577f9d31b89dfd68e
reuse vars_of function

diff -r cf6ba350b7ca -r 490a6e6c7379 src/HOLCF/Tools/Domain/domain_constructors.ML
--- a/src/HOLCF/Tools/Domain/domain_constructors.ML	Fri Feb 26 10:06:24 2010 -0800
+++ b/src/HOLCF/Tools/Domain/domain_constructors.ML	Fri Feb 26 10:11:37 2010 -0800
@@ -321,16 +321,17 @@
     (* get theorems about rep and abs *)
     val abs_strict = iso_locale RS @{thm iso.abs_strict};
 
+    fun vars_of args =
+      let
+        val Ts = map snd args;
+        val ns = Datatype_Prop.make_tnames Ts;
+      in
+        map Free (ns ~~ Ts)
+      end;
+
     (* define constructor functions *)
     val ((con_consts, con_defs), thy) =
       let
-        fun vars_of args =
-          let
-            val Ts = map snd args;
-            val ns = Datatype_Prop.make_tnames Ts;
-          in
-            map Free (ns ~~ Ts)
-          end;
         fun one_arg (lazy, T) var = if lazy then mk_up var else var;
         fun one_con (_,args,_) = mk_stuple (map2 one_arg args (vars_of args));
         fun mk_abs t = abs_const ` t;
@@ -359,9 +360,7 @@
            REPEAT (resolve_tac rules 1 ORELSE atac 1)];
         fun con_compact (con, args) =
           let
-            val Ts = map snd args;
-            val ns = Datatype_Prop.make_tnames Ts;
-            val vs = map Free (ns ~~ Ts);
+            val vs = vars_of args;
             val con_app = list_ccomb (con, vs);
             val concl = mk_trp (mk_compact con_app);
             val assms = map (mk_trp o mk_compact) vs;
@@ -378,9 +377,7 @@
       fun con_strict (con, args) = 
         let
           val rules = abs_strict :: @{thms con_strict_rules};
-          val Ts = map snd args;
-          val ns = Datatype_Prop.make_tnames Ts;
-          val vs = map Free (ns ~~ Ts);
+          val vs = vars_of args;
           val nonlazy = map snd (filter_out fst (map fst args ~~ vs));
           fun one_strict v' =
             let
@@ -395,9 +392,7 @@
         let
           fun iff_disj (t, []) = HOLogic.mk_not t
             | iff_disj (t, ts) = mk_eq (t, foldr1 HOLogic.mk_disj ts);
-          val Ts = map snd args;
-          val ns = Datatype_Prop.make_tnames Ts;
-          val vs = map Free (ns ~~ Ts);
+          val vs = vars_of args;
           val nonlazy = map snd (filter_out fst (map fst args ~~ vs));
           val lhs = mk_undef (list_ccomb (con, vs));
           val rhss = map mk_undef nonlazy;