--- a/Nominal/TySch.thy	Thu Mar 18 14:48:27 2010 +0100
+++ b/Nominal/TySch.thy	Thu Mar 18 15:13:20 2010 +0100
@@ -16,16 +16,16 @@
 and tyS =
   All xs::"name set" ty::"t" bind xs in ty
 
-thm t_tyS_fv
-thm t_tyS_eq_iff
-thm t_tyS_bn
-thm t_tyS_perm
-thm t_tyS_induct
-thm t_tyS_distinct
+thm t_tyS.fv
+thm t_tyS.eq_iff
+thm t_tyS.bn
+thm t_tyS.perm
+thm t_tyS.induct
+thm t_tyS.distinct
 
 lemma
   shows "All {a, b} (Fun (Var a) (Var b)) = All {b, a} (Fun (Var a) (Var b))"
-  apply(simp add: t_tyS_eq_iff)
+  apply(simp add: t_tyS.eq_iff)
   apply(rule_tac x="0::perm" in exI)
   apply(simp add: alpha_gen)
   apply(auto)
@@ -34,7 +34,7 @@
 
 lemma
   shows "All {a, b} (Fun (Var a) (Var b)) = All {a, b} (Fun (Var b) (Var a))"
-  apply(simp add: t_tyS_eq_iff)
+  apply(simp add: t_tyS.eq_iff)
   apply(rule_tac x="(atom a \<rightleftharpoons> atom b)" in exI)
   apply(simp add: alpha_gen fresh_star_def eqvts)
   apply auto
@@ -42,18 +42,18 @@
 
 lemma
   shows "All {a, b, c} (Fun (Var a) (Var b)) = All {a, b} (Fun (Var a) (Var b))"
-  apply(simp add: t_tyS_eq_iff)
+  apply(simp add: t_tyS.eq_iff)
   apply(rule_tac x="0::perm" in exI)
-  apply(simp add: alpha_gen fresh_star_def eqvts t_tyS_eq_iff)
+  apply(simp add: alpha_gen fresh_star_def eqvts t_tyS.eq_iff)
 oops
 
 lemma
   assumes a: "a \<noteq> b"
   shows "\<not>(All {a, b} (Fun (Var a) (Var b)) = All {c} (Fun (Var c) (Var c)))"
   using a
-  apply(simp add: t_tyS_eq_iff)
+  apply(simp add: t_tyS.eq_iff)
   apply(clarify)
-  apply(simp add: alpha_gen fresh_star_def eqvts t_tyS_eq_iff)
+  apply(simp add: alpha_gen fresh_star_def eqvts t_tyS.eq_iff)
   apply auto
   done