diff -r 4939494ed791 -r ce654b0e6d69 src/HOL/MicroJava/Comp/CorrComp.thy
--- a/src/HOL/MicroJava/Comp/CorrComp.thy	Tue Feb 13 14:24:50 2018 +0100
+++ b/src/HOL/MicroJava/Comp/CorrComp.thy	Thu Feb 15 12:11:00 2018 +0100
@@ -740,7 +740,7 @@
 
                     (* case NewC *)
                     apply clarify
-                    apply (frule wf_prog_ws_prog [THEN wf_subcls1]) (* establish  wf ((subcls1 G)^-1) *)
+                    apply (frule wf_prog_ws_prog [THEN wf_subcls1]) (* establish  wf ((subcls1 G)\<inverse>) *)
                     apply (simp add: c_hupd_hp_invariant)
                     apply (rule progression_one_step)
                     apply (rotate_tac 1, drule sym) (* reverse equation (a, None) = new_Addr (fst s) *)