diff -r a3690aeb79d4 -r f3cafd2929d5 src/HOL/MicroJava/J/Conform.thy
--- a/src/HOL/MicroJava/J/Conform.thy	Fri Aug 29 13:18:45 2003 +0200
+++ b/src/HOL/MicroJava/J/Conform.thy	Fri Aug 29 15:19:02 2003 +0200
@@ -120,9 +120,9 @@
 lemma defval_conf [rule_format (no_asm)]: 
   "is_type G T --> G,h\<turnstile>default_val T::\<preceq>T"
 apply (unfold conf_def)
-apply (rule_tac "y" = "T" in ty.exhaust)
+apply (rule_tac y = "T" in ty.exhaust)
 apply  (erule ssubst)
-apply  (rule_tac "y" = "prim_ty" in prim_ty.exhaust)
+apply  (rule_tac y = "prim_ty" in prim_ty.exhaust)
 apply    (auto simp add: widen.null)
 done
 
@@ -178,7 +178,7 @@
 lemma non_np_objD' [rule_format (no_asm)]: 
   "a' \<noteq> Null ==> wf_prog wf_mb G ==> G,h\<turnstile>a'::\<preceq>RefT t --> 
   (\<exists>a C fs. a' = Addr a \<and>  h a = Some (C,fs) \<and>  G\<turnstile>Class C\<preceq>RefT t)"
-apply(rule_tac "y" = "t" in ref_ty.exhaust)
+apply(rule_tac y = "t" in ref_ty.exhaust)
  apply (fast dest: conf_NullTD)
 apply (fast dest: non_np_objD)
 done