use y as variable name in casedist, like datatype package
authorhuffman
Tue, 02 Mar 2010 17:34:03 -0800
changeset 35526 85e9423d7deb
parent 35525 fa231b86cb1e
child 35527 f4282471461d
use y as variable name in casedist, like datatype package
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})],