diff -r c9a1c6f50ff5 -r cf451e182bf0 Slides/Slides9.thy
--- a/Slides/Slides9.thy	Fri Sep 06 10:06:41 2013 +0100
+++ b/Slides/Slides9.thy	Sun Oct 13 23:09:21 2013 +0200
@@ -1,6 +1,6 @@
 (*<*)
 theory Slides9
-imports "~~/src/HOL/Library/LaTeXsugar" "Nominal"
+imports "~~/src/HOL/Library/LaTeXsugar" "../Nominal/Nominal2"
 begin
 
 notation (latex output)