# HG changeset patch
# User huffman
# Date 1267580043 28800
# Node ID 85e9423d7debc891bcd5ccb92107edfe8656f9ab
# Parent  fa231b86cb1e7ef78ad31fc67cddf1f3059cfe87
use y as variable name in casedist, like datatype package

diff -r fa231b86cb1e -r 85e9423d7deb src/HOLCF/Tools/Domain/domain_constructors.ML
--- a/src/HOLCF/Tools/Domain/domain_constructors.ML	Tue Mar 02 17:21:10 2010 -0800
+++ b/src/HOLCF/Tools/Domain/domain_constructors.ML	Tue Mar 02 17:34:03 2010 -0800
@@ -190,15 +190,15 @@
       val thm2 = rewrite_rule (map mk_meta_eq @{thms ex_defined_iffs}) thm1;
       val thm3 = rewrite_rule [mk_meta_eq @{thm conj_assoc}] thm2;
 
-      val x = Free ("x", lhsT);
+      val y = Free ("y", lhsT);
       fun one_con (con, args) =
         let
-          val (vs, nonlazy) = get_vars_avoiding ["x"] args;
-          val eqn = mk_eq (x, list_ccomb (con, vs));
+          val (vs, nonlazy) = get_vars_avoiding ["y"] args;
+          val eqn = mk_eq (y, list_ccomb (con, vs));
           val conj = foldr1 mk_conj (eqn :: map mk_defined nonlazy);
         in Library.foldr mk_ex (vs, conj) end;
-      val goal = mk_trp (foldr1 mk_disj (mk_undef x :: map one_con spec'));
-      (* first 3 rules replace "x = UU \/ P" with "rep$x = UU \/ P" *)
+      val goal = mk_trp (foldr1 mk_disj (mk_undef y :: map one_con spec'));
+      (* first 3 rules replace "y = UU \/ P" with "rep$y = UU \/ P" *)
       val tacs = [
           rtac (iso_locale RS @{thm iso.casedist_rule}) 1,
           rewrite_goals_tac [mk_meta_eq (iso_locale RS @{thm iso.iso_swap})],