# HG changeset patch
# User huffman
# Date 1267587937 28800
# Node ID 297e801b54658de20e8e597cc32ffade10bab7b6
# Parent  f4282471461da062bd727696f4e61eafbb03fcf0
proof scripts use variable name y for casedist

diff -r f4282471461d -r 297e801b5465 src/HOLCF/Tools/Domain/domain_theorems.ML
--- a/src/HOLCF/Tools/Domain/domain_theorems.ML	Tue Mar 02 18:16:28 2010 -0800
+++ b/src/HOLCF/Tools/Domain/domain_theorems.ML	Tue Mar 02 19:45:37 2010 -0800
@@ -424,7 +424,7 @@
             map (K (atac 1)) (nonlazy args) @
             map (K (etac spec 1)) (filter is_rec args);
           fun cases_tacs (cons, cases) =
-            res_inst_tac context [(("x", 0), "x")] cases 1 ::
+            res_inst_tac context [(("y", 0), "x")] cases 1 ::
             asm_simp_tac (take_ss addsimps prems) 1 ::
             maps con_tacs cons;
         in
@@ -499,7 +499,7 @@
             fun foo_tacs ctxt n (cons, cases) =
               simp_tac take_ss 1 ::
               rtac allI 1 ::
-              res_inst_tac ctxt [(("x", 0), x_name n)] cases 1 ::
+              res_inst_tac ctxt [(("y", 0), x_name n)] cases 1 ::
               asm_simp_tac take_ss 1 ::
               maps (con_tacs ctxt) cons;
             fun tacs ctxt =