diff -r 7ce5fcebfb35 -r a39ef48fbee0 src/HOL/MicroJava/Comp/CorrComp.thy
--- a/src/HOL/MicroJava/Comp/CorrComp.thy	Fri Apr 21 16:48:12 2017 +0200
+++ b/src/HOL/MicroJava/Comp/CorrComp.thy	Fri Apr 21 16:48:58 2017 +0200
@@ -5,7 +5,7 @@
 (* Compiler correctness statement and proof *)
 
 theory CorrComp
-imports "../J/JTypeSafe" "LemmasComp"
+imports "../J/JTypeSafe" LemmasComp
 begin
 
 declare wf_prog_ws_prog [simp add]