diff -r ac69ed8303cc -r 304bd7400a47 Nominal/ExTySch.thy
--- a/Nominal/ExTySch.thy	Tue Mar 23 10:24:12 2010 +0100
+++ b/Nominal/ExTySch.thy	Tue Mar 23 10:26:46 2010 +0100
@@ -86,10 +86,10 @@
     apply simp
     apply (rule allI)
     apply (rule allI)
-    apply(subgoal_tac "\<exists>pa. ((pa \<bullet> (fset_to_set (fmap atom (p \<bullet> fset)))) \<sharp>* d \<and> supp (p \<bullet> TySch.All fset t) \<sharp>* pa)")
+    apply(subgoal_tac "\<exists>pa. ((pa \<bullet> (fset_to_set (fmap atom (p \<bullet> fset)))) \<sharp>* d \<and> supp (p \<bullet> All fset t) \<sharp>* pa)")
     apply clarify
-    apply(rule_tac t="p \<bullet> TySch.All fset t" and 
-                   s="pa \<bullet> (p \<bullet> TySch.All fset t)" in subst)
+    apply(rule_tac t="p \<bullet> All fset t" and 
+                   s="pa \<bullet> (p \<bullet> All fset t)" in subst)
     apply (rule supp_perm_eq)
     apply assumption
     apply (simp only: t_tyS.perm)