diff -r 4af8a92396ce -r a44479bde681 Nominal/Nominal2_Base.thy
--- a/Nominal/Nominal2_Base.thy	Mon Jul 20 11:21:59 2015 +0100
+++ b/Nominal/Nominal2_Base.thy	Tue Mar 22 12:18:30 2016 +0000
@@ -13,6 +13,9 @@
   "atom_decl" "equivariance" :: thy_decl 
 begin
 
+declare [[typedef_overloaded]]
+
+
 section {* Atoms and Sorts *}
 
 text {* A simple implementation for atom_sorts is strings. *}
@@ -183,7 +186,7 @@
   by (simp add: Abs_perm_inverse perm_inv Rep_perm)
 
 instance
-apply default
+apply standard
 unfolding Rep_perm_inject [symmetric]
 unfolding minus_perm_def
 unfolding Rep_perm_add
@@ -325,7 +328,7 @@
   "p \<bullet> a = (Rep_perm p) a"
 
 instance 
-apply(default)
+apply standard
 apply(simp_all add: permute_atom_def Rep_perm_simps)
 done
 
@@ -363,7 +366,7 @@
   "p \<bullet> q = p + q - p"
 
 instance
-apply default
+apply standard
 apply (simp add: permute_perm_def)
 apply (simp add: permute_perm_def algebra_simps)
 done
@@ -390,7 +393,7 @@
   "p \<bullet> f = (\<lambda>x. p \<bullet> (f (- p \<bullet> x)))"
 
 instance
-apply default
+apply standard
 apply (simp add: permute_fun_def)
 apply (simp add: permute_fun_def minus_add)
 done
@@ -413,7 +416,7 @@
 definition "p \<bullet> (b::bool) = b"
 
 instance
-apply(default) 
+apply standard
 apply(simp_all add: permute_bool_def)
 done
 
@@ -438,7 +441,7 @@
   "p \<bullet> X = {p \<bullet> x | x. x \<in> X}" 
 
 instance
-apply default
+apply standard
 apply (auto simp: permute_set_def)
 done
 
@@ -510,7 +513,7 @@
 definition "p \<bullet> (u::unit) = u"
 
 instance 
-by (default) (simp_all add: permute_unit_def)
+  by standard (simp_all add: permute_unit_def)
 
 end
 
@@ -526,7 +529,7 @@
   Pair_eqvt: "p \<bullet> (x, y) = (p \<bullet> x, p \<bullet> y)"
 
 instance
-by default auto
+  by standard auto
 
 end
 
@@ -542,7 +545,7 @@
 | Inr_eqvt: "p \<bullet> (Inr y) = Inr (p \<bullet> y)"
 
 instance 
-by (default) (case_tac [!] x, simp_all)
+  by standard (case_tac [!] x, simp_all)
 
 end
 
@@ -558,7 +561,7 @@
 | Cons_eqvt: "p \<bullet> (x # xs) = p \<bullet> x # p \<bullet> xs"
 
 instance 
-by (default) (induct_tac [!] x, simp_all)
+  by standard (induct_tac [!] x, simp_all)
 
 end
 
@@ -580,7 +583,7 @@
 | Some_eqvt: "p \<bullet> (Some x) = Some (p \<bullet> x)"
 
 instance 
-by (default) (induct_tac [!] x, simp_all)
+  by standard (induct_tac [!] x, simp_all)
 
 end
 
@@ -667,7 +670,7 @@
   done
 
 instance
-apply(default)
+apply standard
 apply(transfer)
 apply(simp)
 apply(transfer)
@@ -685,7 +688,7 @@
 definition "p \<bullet> (c::char) = c"
 
 instance 
-by (default) (simp_all add: permute_char_def)
+  by standard (simp_all add: permute_char_def)
 
 end
 
@@ -695,7 +698,7 @@
 definition "p \<bullet> (n::nat) = n"
 
 instance 
-by (default) (simp_all add: permute_nat_def)
+  by standard (simp_all add: permute_nat_def)
 
 end
 
@@ -705,7 +708,7 @@
 definition "p \<bullet> (i::int) = i"
 
 instance 
-by (default) (simp_all add: permute_int_def)
+  by standard (simp_all add: permute_int_def)
 
 end
 
@@ -729,22 +732,22 @@
 text {* Other type constructors preserve purity. *}
 
 instance "fun" :: (pure, pure) pure
-by default (simp add: permute_fun_def permute_pure)
+  by standard (simp add: permute_fun_def permute_pure)
 
 instance set :: (pure) pure
-by default (simp add: permute_set_def permute_pure)
+  by standard (simp add: permute_set_def permute_pure)
 
 instance prod :: (pure, pure) pure
-by default (induct_tac x, simp add: permute_pure)
+  by standard (induct_tac x, simp add: permute_pure)
 
 instance sum :: (pure, pure) pure
-by default (induct_tac x, simp_all add: permute_pure)
+  by standard (induct_tac x, simp_all add: permute_pure)
 
 instance list :: (pure) pure
-by default (induct_tac x, simp_all add: permute_pure)
+  by standard (induct_tac x, simp_all add: permute_pure)
 
 instance option :: (pure) pure
-by default (induct_tac x, simp_all add: permute_pure)
+  by standard (induct_tac x, simp_all add: permute_pure)
 
 
 subsection {* Types @{typ char}, @{typ nat}, and @{typ int} *}
@@ -1069,7 +1072,7 @@
 begin
 
 instance 
-apply(default)
+apply standard
 unfolding le_bool_def
 apply(perm_simp)
 apply(rule refl)
@@ -1081,7 +1084,7 @@
 begin
 
 instance 
-apply(default)
+apply standard
 unfolding le_fun_def
 apply(perm_simp)
 apply(rule refl)
@@ -1093,7 +1096,7 @@
 begin
 
 instance 
-apply(default)
+apply standard
 unfolding Inf_bool_def
 apply(perm_simp)
 apply(rule refl)
@@ -1105,7 +1108,7 @@
 begin
 
 instance 
-apply(default)
+apply standard
 unfolding Inf_fun_def INF_def
 apply(perm_simp)
 apply(rule refl)
@@ -1145,7 +1148,7 @@
   by (cases x) simp
 
 lemma split_eqvt [eqvt]: 
-  shows "p \<bullet> (split P x) = split (p \<bullet> P) (p \<bullet> x)"
+  shows "p \<bullet> (case_prod P x) = case_prod (p \<bullet> P) (p \<bullet> x)"
   unfolding split_def
   by simp
 
@@ -1456,7 +1459,7 @@
   unfolding fresh_def by (simp add: pure_supp)
 
 instance pure < fs
-by default (simp add: pure_supp)
+  by standard (simp add: pure_supp)
 
 
 subsection  {* Type @{typ atom} is finitely-supported. *}
@@ -1474,7 +1477,7 @@
   unfolding fresh_def supp_atom by simp
 
 instance atom :: fs
-by default (simp add: supp_atom)
+  by standard (simp add: supp_atom)
 
 
 section {* Type @{typ perm} is finitely-supported. *}
@@ -1623,7 +1626,7 @@
 
 
 instance perm :: fs
-by default (simp add: supp_perm finite_perm_lemma)
+  by standard (simp add: supp_perm finite_perm_lemma)
 
 
 
@@ -1649,7 +1652,7 @@
   by (simp add: fresh_def supp_Unit)
 
 instance prod :: (fs, fs) fs
-apply default
+apply standard
 apply (case_tac x)
 apply (simp add: supp_Pair finite_supp)
 done
@@ -1674,7 +1677,7 @@
   by (simp add: fresh_def supp_Inr)
 
 instance sum :: (fs, fs) fs
-apply default
+apply standard
 apply (case_tac x)
 apply (simp_all add: supp_Inl supp_Inr finite_supp)
 done
@@ -1699,7 +1702,7 @@
   by (simp add: fresh_def supp_Some)
 
 instance option :: (fs) fs
-apply default
+apply standard
 apply (induct_tac x)
 apply (simp_all add: supp_None supp_Some finite_supp)
 done
@@ -1752,7 +1755,7 @@
    (simp_all add: supp_Nil supp_Cons supp_atom)
 
 instance list :: (fs) fs
-apply default
+apply standard
 apply (induct_tac x)
 apply (simp_all add: supp_Nil supp_Cons finite_supp)
 done
@@ -1895,7 +1898,7 @@
         val cty_inst =
           [SOME (Thm.ctyp_of ctxt (fastype_of argx)), SOME (Thm.ctyp_of ctxt (fastype_of f))]
         val ctrm_inst = [NONE, SOME (Thm.cterm_of ctxt absf), SOME (Thm.cterm_of ctxt argx)] 
-        val thm = Drule.instantiate' cty_inst ctrm_inst @{thm fresh_fun_app}
+        val thm = Thm.instantiate' cty_inst ctrm_inst @{thm fresh_fun_app}
       in
         SOME(thm RS @{thm Eq_TrueI}) 
       end  
@@ -2120,12 +2123,12 @@
 
 subsection {* Type @{typ "'a multiset"} is finitely supported *}
 
-lemma set_of_eqvt [eqvt]:
-  shows "p \<bullet> (set_of M) = set_of (p \<bullet> M)"
+lemma set_mset_eqvt [eqvt]:
+  shows "p \<bullet> (set_mset M) = set_mset (p \<bullet> M)"
 by (induct M) (simp_all add: insert_eqvt empty_eqvt)
 
-lemma supp_set_of:
-  shows "supp (set_of M) \<subseteq> supp M"
+lemma supp_set_mset:
+  shows "supp (set_mset M) \<subseteq> supp M"
   apply (rule supp_fun_app_eqvt)
   unfolding eqvt_def
   apply(perm_simp)
@@ -2165,11 +2168,11 @@
   fixes M::"('a::fs multiset)" 
   shows "(\<Union>{supp x | x. x \<in># M}) \<subseteq> supp M"
 proof -
-  have "(\<Union>{supp x | x. x \<in># M}) = (\<Union>{supp x | x. x \<in> set_of M})" by simp
-  also have "... \<subseteq> (\<Union>x \<in> set_of M. supp x)" by auto
-  also have "... = supp (set_of M)"
+  have "(\<Union>{supp x | x. x \<in># M}) = (\<Union>{supp x | x. x \<in> set_mset M})" by simp
+  also have "... \<subseteq> (\<Union>x \<in> set_mset M. supp x)" by auto
+  also have "... = supp (set_mset M)"
     by (simp add: supp_of_finite_sets)
-  also have " ... \<subseteq> supp M" by (rule supp_set_of)
+  also have " ... \<subseteq> supp M" by (rule supp_set_mset)
   finally show "(\<Union>{supp x | x. x \<in># M}) \<subseteq> supp M" .
 qed
 
@@ -2199,9 +2202,7 @@
   by simp
 
 instance multiset :: (fs) fs
-  apply (default)
-  apply (rule multisets_supp_finite)
-  done
+  by standard (rule multisets_supp_finite)
 
 subsection {* Type @{typ "'a fset"} is finitely supported *}
 
@@ -2252,9 +2253,7 @@
 by (simp add: supp_union_fset)
 
 instance fset :: (fs) fs
-  apply (default)
-  apply (rule fset_finite_supp)
-  done
+  by standard (rule fset_finite_supp)
 
 
 subsection {* Type @{typ "('a, 'b) finfun"} is finitely supported *}
@@ -2279,7 +2278,7 @@
 by (auto simp: fresh_def supp_Pair)
     
 instance finfun :: (fs, fs) fs
-  apply(default)
+  apply standard
   apply(induct_tac x rule: finfun_weak_induct)
   apply(simp add: supp_finfun_const finite_supp)
   apply(rule finite_subset)