diff -r 9fc50a3e07f6 -r 403dd13cf6e9 src/HOL/IMP/Compiler2.thy
--- a/src/HOL/IMP/Compiler2.thy	Fri Aug 17 11:26:35 2018 +0000
+++ b/src/HOL/IMP/Compiler2.thy	Mon Aug 20 20:54:26 2018 +0200
@@ -1,16 +1,16 @@
 (* Author: Gerwin Klein *)
 
+section \<open>Compiler Correctness, Reverse Direction\<close>
+
 theory Compiler2
 imports Compiler
 begin
 
 text \<open>
 The preservation of the source code semantics is already shown in the 
-parent theory @{theory "HOL-IMP.Compiler"}. This here shows the second direction.
+parent theory @{text "Compiler"}. This here shows the second direction.
 \<close>
 
-section \<open>Compiler Correctness, Reverse Direction\<close>
-
 subsection \<open>Definitions\<close>
 
 text \<open>Execution in @{term n} steps for simpler induction\<close>