# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1269333483 -3600
# Node ID d46a32cfcd89cf9a08c039e57647e3ef53503b5d
# Parent  5ab97f43ec244dcb8c5e55cef7166640b3d952bd
compiles

diff -r 5ab97f43ec24 -r d46a32cfcd89 Nominal/ExTySch.thy
--- a/Nominal/ExTySch.thy	Tue Mar 23 09:34:32 2010 +0100
+++ b/Nominal/ExTySch.thy	Tue Mar 23 09:38:03 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)