renamed variable in cont2cont_app
authorhuffman
Fri, 03 Jun 2005 23:35:18 +0200
changeset 16216 279ab2e02089
parent 16215 7ff978ca1920
child 16217 96f0c8546265
renamed variable in cont2cont_app
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)