diff -r 9df4b3934487 -r fe20540bcf93 src/HOL/IMP/Compiler.thy
--- a/src/HOL/IMP/Compiler.thy	Thu Dec 20 17:08:55 2001 +0100
+++ b/src/HOL/IMP/Compiler.thy	Thu Dec 20 18:22:44 2001 +0100
@@ -135,7 +135,7 @@
 subsection "Compiler correctness"
 
 declare rtrancl_into_rtrancl[trans]
-        rtrancl_into_rtrancl2[trans]
+        converse_rtrancl_into_rtrancl[trans]
         rtrancl_trans[trans]
 
 text {*
@@ -232,7 +232,7 @@
    apply(erule_tac x = "a@[?I]" in allE)
    apply(simp)
    (* execute JMPF: *)
-   apply(rule rtrancl_into_rtrancl2)
+   apply(rule converse_rtrancl_into_rtrancl)
     apply(force intro!: JMPFT)
    (* execute compile c0: *)
    apply(rule rtrancl_trans)
@@ -245,7 +245,7 @@
   apply(intro strip)
   apply(erule_tac x = "a@[?I]@compile c0@[?J]" in allE)
   apply(simp add:add_assoc)
-  apply(rule rtrancl_into_rtrancl2)
+  apply(rule converse_rtrancl_into_rtrancl)
    apply(force intro!: JMPFF)
   apply(blast)
  apply(force intro: JMPFF)
@@ -253,12 +253,12 @@
 apply(erule_tac x = "a@[?I]" in allE)
 apply(erule_tac x = a in allE)
 apply(simp)
-apply(rule rtrancl_into_rtrancl2)
+apply(rule converse_rtrancl_into_rtrancl)
  apply(force intro!: JMPFT)
 apply(rule rtrancl_trans)
  apply(erule allE)
  apply assumption
-apply(rule rtrancl_into_rtrancl2)
+apply(rule converse_rtrancl_into_rtrancl)
  apply(force intro!: JMPB)
 apply(simp)
 done