# HG changeset patch
# User huffman
# Date 1117834518 -7200
# Node ID 279ab2e02089555be007a31e018969fdcdaf1037
# Parent  7ff978ca1920a864f2aececdea2feb92e2f9cf0d
renamed variable in cont2cont_app

diff -r 7ff978ca1920 -r 279ab2e02089 src/HOLCF/Lift.thy
--- a/src/HOLCF/Lift.thy	Fri Jun 03 23:34:49 2005 +0200
+++ b/src/HOLCF/Lift.thy	Fri Jun 03 23:35:18 2005 +0200
@@ -247,7 +247,7 @@
     cont (%y. lift_case UU (f y) (g y))"
   -- {* @{text flift1} is continuous in a variable that occurs either
     in the @{text Def} branch or in the argument. *}
-  apply (rule_tac tt = g in cont2cont_app)
+  apply (rule_tac t=g in cont2cont_app)
     apply (rule cont_flift1_not_arg)
     apply auto
   apply (rule cont_flift1_arg)