| changeset 58184 | db1381d811ab |
| parent 56154 | f0a927235162 |
| child 59199 | cb8e5f7a5e4a |
--- a/src/HOL/MicroJava/Comp/LemmasComp.thy Thu Sep 04 11:53:39 2014 +0200 +++ b/src/HOL/MicroJava/Comp/LemmasComp.thy Thu Sep 04 14:02:37 2014 +0200 @@ -200,7 +200,7 @@ (* case class G x = None *) apply (simp (no_asm_simp) add: class_rec_def comp_subcls1 - wfrec [where r="(subcls1 G)^-1", simplified]) + wfrec [where R="(subcls1 G)^-1", simplified]) apply (simp add: comp_class_None) (* case \<exists> D fs ms. (class G x = Some (D, fs, ms)) *)