diff -r a3690aeb79d4 -r f3cafd2929d5 src/HOL/NanoJava/Equivalence.thy
--- a/src/HOL/NanoJava/Equivalence.thy	Fri Aug 29 13:18:45 2003 +0200
+++ b/src/HOL/NanoJava/Equivalence.thy	Fri Aug 29 15:19:02 2003 +0200
@@ -83,7 +83,7 @@
 lemma Loop_sound_lemma [rule_format (no_asm)]: 
 "\<forall>s t. s -c-n\<rightarrow> t \<longrightarrow> P s \<and> s<x> \<noteq> Null \<longrightarrow> P t \<Longrightarrow> 
   (s -c0-n0\<rightarrow> t \<longrightarrow> P s \<longrightarrow> c0 = While (x) c \<longrightarrow> n0 = n \<longrightarrow> P t \<and> t<x> = Null)"
-apply (rule_tac "P2.1"="%s e v n t. True" in exec_eval.induct [THEN conjunct1])
+apply (rule_tac ?P2.1="%s e v n t. True" in exec_eval.induct [THEN conjunct1])
 apply clarsimp+
 done