diff -r e903c32ec24f -r 693562f03eee Nominal/Ex/TypeSchemes.thy
--- a/Nominal/Ex/TypeSchemes.thy	Wed Oct 13 22:55:58 2010 +0100
+++ b/Nominal/Ex/TypeSchemes.thy	Thu Oct 14 04:14:22 2010 +0100
@@ -56,7 +56,7 @@
 lemma strong_induct:
   assumes a1: "\<And>name b. P b (Var name)"
   and     a2: "\<And>t1 t2 b. \<lbrakk>\<And>c. P c t1; \<And>c. P c t2\<rbrakk> \<Longrightarrow> P b (Fun t1 t2)"
-  and     a3: "\<And>fset t b. \<lbrakk>\<And>c. P c t; fset_to_set (fmap atom fset) \<sharp>* b\<rbrakk> \<Longrightarrow> P' b (All fset t)"
+  and     a3: "\<And>fset t b. \<lbrakk>\<And>c. P c t; fset (fmap atom fset) \<sharp>* b\<rbrakk> \<Longrightarrow> P' b (All fset t)"
   shows "P (a :: 'a :: pt) t \<and> P' (d :: 'b :: {fs}) ts "
 proof -
   have " (\<forall>p a. P a (p \<bullet> t)) \<and> (\<forall>p d. P' d (p \<bullet> ts))"
@@ -69,7 +69,7 @@
     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> All fset ty) \<sharp>* pa)")
+    apply(subgoal_tac "\<exists>pa. ((pa \<bullet> (fset (fmap atom (p \<bullet> fset)))) \<sharp>* d \<and> supp (p \<bullet> All fset ty) \<sharp>* pa)")
     apply clarify
     apply(rule_tac t="p \<bullet> All fset ty" and 
                    s="pa \<bullet> (p \<bullet> All fset ty)" in subst)
@@ -81,7 +81,7 @@
     apply simp
     apply (simp add: eqvts eqvts_raw)
     apply (rule at_set_avoiding2)
-    apply (simp add: fin_fset_to_set)
+    apply (simp add: fin_fset)
     apply (simp add: finite_supp)
     apply (simp add: eqvts finite_supp)
     apply (rule_tac p=" -p" in permute_boolE)
@@ -142,7 +142,7 @@
 assumes
     s1: "subst \<theta> (Var n) = lookup \<theta> n"
 and s2: "subst \<theta> (Fun l r) = Fun (subst \<theta> l) (subst \<theta> r)"
-and s3: "fset_to_set (fmap atom xs) \<sharp>* \<theta> \<Longrightarrow> substs \<theta> (All xs t) = All xs (subst \<theta> t)"
+and s3: "fset (fmap atom xs) \<sharp>* \<theta> \<Longrightarrow> substs \<theta> (All xs t) = All xs (subst \<theta> t)"
 begin
 
 lemma subst_ty:
@@ -163,7 +163,7 @@
   apply (simp_all add: fresh_star_prod_elim)
   apply (drule fresh_star_atom)
   apply (simp add: fresh_def ty_tys.fv[simplified ty_tys.supp])
-  apply (subgoal_tac "atom a \<notin> fset_to_set (fmap atom fset)")
+  apply (subgoal_tac "atom a \<notin> fset (fmap atom fset)")
   apply blast
   apply (metis supp_finite_atom_set finite_fset)
   done
@@ -197,7 +197,7 @@
   apply (fold fresh_def)[1]
   apply (rule mp[OF subst_lemma_pre])
   apply (simp add: fresh_Pair)
-  apply (subgoal_tac "atom a \<notin> (fset_to_set (fmap atom fset))")
+  apply (subgoal_tac "atom a \<notin> (fset (fmap atom fset))")
   apply blast
   apply (metis supp_finite_atom_set finite_fset)
   done