diff -r c9a1c6f50ff5 -r cf451e182bf0 Slides/Slides2.thy
--- a/Slides/Slides2.thy	Fri Sep 06 10:06:41 2013 +0100
+++ b/Slides/Slides2.thy	Sun Oct 13 23:09:21 2013 +0200
@@ -1,6 +1,6 @@
 (*<*)
 theory Slides2
-imports "~~/src/HOL/Library/LaTeXsugar" "Nominal"
+imports "~~/src/HOL/Library/LaTeXsugar" "../Nominal/Nominal2"
 begin
 
 notation (latex output)
@@ -385,7 +385,7 @@
 
   {\small\begin{tabular}{rcl}
   @{text "sort_ty (TVar x)"}  & @{text "\<equiv>"} & @{text "Sort ''TVar'' [Sort x []]"} \\
-  @{text "sort_ty (\<tau>\<^isub>1 \<rightarrow> \<tau>\<^isub>2)"} & @{text "\<equiv>"} & @{text "Sort ''Fun'' [sort_ty \<tau>\<^isub>1, sort_ty \<tau>\<^isub>2]"}\\
+  @{text "sort_ty (\<tau>\<^sub>1 \<rightarrow> \<tau>\<^sub>2)"} & @{text "\<equiv>"} & @{text "Sort ''Fun'' [sort_ty \<tau>\<^sub>1, sort_ty \<tau>\<^sub>2]"}\\
   \end{tabular}}
   \pause
   \isanewline\isanewline