src/HOLCF/Tools/Domain/domain_constructors.ML

     (* prove strictness rules for constructors *)
     local
       fun con_strict (con, args) = 
         let
           val rules = abs_strict :: @{thms con_strict_rules};
-          val vs = vars_of args;
-          val nonlazy = map snd (filter_out fst (map fst args ~~ vs));
+          val (vs, nonlazy) = get_vars args;
           fun one_strict v' =
             let
               val UU = mk_bottom (fastype_of v');
               val vs' = map (fn v => if v = v' then UU else v) vs;
               val goal = mk_trp (mk_undef (list_ccomb (con, vs')));

 
       fun con_defin (con, args) =
         let
           fun iff_disj (t, []) = HOLogic.mk_not t
             | iff_disj (t, ts) = mk_eq (t, foldr1 HOLogic.mk_disj ts);
-          val vs = vars_of args;
-          val nonlazy = map snd (filter_out fst (map fst args ~~ vs));
+          val (vs, nonlazy) = get_vars args;
           val lhs = mk_undef (list_ccomb (con, vs));
           val rhss = map mk_undef nonlazy;
           val goal = mk_trp (iff_disj (lhs, rhss));
           val rule1 = iso_locale RS @{thm iso.abs_defined_iff};
           val rules = rule1 :: @{thms con_defined_iff_rules};

     local
       fun pgterm rel (con, args) =
         let
           fun prime (Free (n, T)) = Free (n^"'", T)
             | prime t             = t;
-          val xs = vars_of args;
+          val (xs, nonlazy) = get_vars args;
           val ys = map prime xs;
-          val nonlazy = map snd (filter_out (fst o fst) (args ~~ xs));
           val lhs = rel (list_ccomb (con, xs), list_ccomb (con, ys));
           val rhs = foldr1 mk_conj (ListPair.map rel (xs, ys));
           val concl = mk_trp (mk_eq (lhs, rhs));
           val zs = case args of [_] => [] | _ => nonlazy;
           val assms = map (mk_trp o mk_defined) zs;

         | iff_disj2 (t, ts, []) = mk_not t
         | iff_disj2 (t, ts, us) =
           mk_eq (t, mk_conj (foldr1 mk_disj ts, foldr1 mk_disj us));
       fun dist_le (con1, args1) (con2, args2) =
         let
-          val vs1 = vars_of args1;
-          val vs2 = map prime (vars_of args2);
-          val zs1 = map snd (filter_out (fst o fst) (args1 ~~ vs1));
+          val (vs1, zs1) = get_vars args1;
+          val (vs2, zs2) = get_vars args2 |> pairself (map prime);
           val lhs = mk_below (list_ccomb (con1, vs1), list_ccomb (con2, vs2));
           val rhss = map mk_undef zs1;
           val goal = mk_trp (iff_disj (lhs, rhss));
           val rule1 = iso_locale RS @{thm iso.abs_below};
           val rules = rule1 :: @{thms con_below_iff_rules};
           val tacs = [simp_tac (HOL_ss addsimps rules) 1];
         in prove thy con_betas goal (K tacs) end;
       fun dist_eq (con1, args1) (con2, args2) =
         let
-          val vs1 = vars_of args1;
-          val vs2 = map prime (vars_of args2);
-          val zs1 = map snd (filter_out (fst o fst) (args1 ~~ vs1));
-          val zs2 = map snd (filter_out (fst o fst) (args2 ~~ vs2));
+          val (vs1, zs1) = get_vars args1;
+          val (vs2, zs2) = get_vars args2 |> pairself (map prime);
           val lhs = mk_eq (list_ccomb (con1, vs1), list_ccomb (con2, vs2));
           val rhss1 = map mk_undef zs1;
           val rhss2 = map mk_undef zs2;
           val goal = mk_trp (iff_disj2 (lhs, rhss1, rhss2));
           val rule1 = iso_locale RS @{thm iso.abs_eq};