# HG changeset patch
# User berghofe
# Date 1210150639 -7200
# Node ID 40b411ec05aadaa7858b76c524fa42acc42f1029
# Parent  27941d7d9a11eaeddc5188661485682a903cbfc5
Adapted to encoding of sets as predicates

diff -r 27941d7d9a11 -r 40b411ec05aa doc-src/TutorialI/Sets/Relations.thy
--- a/doc-src/TutorialI/Sets/Relations.thy	Wed May 07 10:56:58 2008 +0200
+++ b/doc-src/TutorialI/Sets/Relations.thy	Wed May 07 10:57:19 2008 +0200
@@ -151,7 +151,7 @@
 text{*Pow, Inter too little used*}
 
 lemma "(A \<subset> B) = (A \<subseteq> B \<and> A \<noteq> B)"
-apply (simp add: psubset_def)
+apply (simp add: psubset_eq)
 done
 
 end
diff -r 27941d7d9a11 -r 40b411ec05aa src/HOL/Algebra/Sylow.thy
--- a/src/HOL/Algebra/Sylow.thy	Wed May 07 10:56:58 2008 +0200
+++ b/src/HOL/Algebra/Sylow.thy	Wed May 07 10:57:19 2008 +0200
@@ -262,7 +262,7 @@
 apply (rule coset_join1 [THEN in_H_imp_eq])
 apply (rule_tac [3] H_is_subgroup)
 prefer 2 apply (blast intro: m_closed M_elem_map_carrier inv_closed)
-apply (simp add: coset_mult_inv2 H_def M_elem_map_carrier subset_def)
+apply (simp add: coset_mult_inv2 H_def M_elem_map_carrier subset_eq)
 done
 
 
diff -r 27941d7d9a11 -r 40b411ec05aa src/HOL/Complex/ex/BigO_Complex.thy
--- a/src/HOL/Complex/ex/BigO_Complex.thy	Wed May 07 10:56:58 2008 +0200
+++ b/src/HOL/Complex/ex/BigO_Complex.thy	Wed May 07 10:57:19 2008 +0200
@@ -42,7 +42,7 @@
   apply (drule set_plus_imp_minus)
   apply (drule bigo_LIMSEQ1)
   apply assumption
-  apply (simp only: func_diff)
+  apply (simp only: fun_diff_def)
   apply (erule LIMSEQ_diff_approach_zero2)
   apply assumption
 done
diff -r 27941d7d9a11 -r 40b411ec05aa src/HOL/Hyperreal/NatStar.thy
--- a/src/HOL/Hyperreal/NatStar.thy	Wed May 07 10:56:58 2008 +0200
+++ b/src/HOL/Hyperreal/NatStar.thy	Wed May 07 10:57:19 2008 +0200
@@ -36,7 +36,7 @@
 by (auto simp add: InternalSets_def starset_n_Int [symmetric])
 
 lemma starset_n_Compl: "*sn* ((%n. - A n)) = -( *sn* A)"
-apply (simp add: starset_n_def star_n_eq_starfun_whn Compl_def)
+apply (simp add: starset_n_def star_n_eq_starfun_whn Compl_eq)
 apply (rule_tac x=whn in spec, transfer, simp)
 done
 
@@ -44,7 +44,7 @@
 by (auto simp add: InternalSets_def starset_n_Compl [symmetric])
 
 lemma starset_n_diff: "*sn* (%n. (A n) - (B n)) = *sn* A - *sn* B"
-apply (simp add: starset_n_def star_n_eq_starfun_whn set_diff_def)
+apply (simp add: starset_n_def star_n_eq_starfun_whn set_diff_eq)
 apply (rule_tac x=whn in spec, transfer, simp)
 done
 
diff -r 27941d7d9a11 -r 40b411ec05aa src/HOL/Hyperreal/StarDef.thy
--- a/src/HOL/Hyperreal/StarDef.thy	Wed May 07 10:56:58 2008 +0200
+++ b/src/HOL/Hyperreal/StarDef.thy	Wed May 07 10:57:19 2008 +0200
@@ -18,7 +18,7 @@
 
 lemma freeultrafilter_FreeUltrafilterNat: "freeultrafilter \<U>"
 apply (unfold FreeUltrafilterNat_def)
-apply (rule someI_ex)
+apply (rule someI_ex [where P=freeultrafilter])
 apply (rule freeultrafilter_Ex)
 apply (rule nat_infinite)
 done
@@ -401,10 +401,10 @@
 by (transfer Int_def, rule refl)
 
 lemma starset_Compl: "*s* -A = -( *s* A)"
-by (transfer Compl_def, rule refl)
+by (transfer Compl_eq, rule refl)
 
 lemma starset_diff: "*s* (A - B) = *s* A - *s* B"
-by (transfer set_diff_def, rule refl)
+by (transfer set_diff_eq, rule refl)
 
 lemma starset_image: "*s* (f ` A) = ( *f* f) ` ( *s* A)"
 by (transfer image_def, rule refl)
@@ -413,7 +413,7 @@
 by (transfer vimage_def, rule refl)
 
 lemma starset_subset: "( *s* A \<subseteq> *s* B) = (A \<subseteq> B)"
-by (transfer subset_def, rule refl)
+by (transfer subset_eq, rule refl)
 
 lemma starset_eq: "( *s* A = *s* B) = (A = B)"
 by (transfer, rule refl)
diff -r 27941d7d9a11 -r 40b411ec05aa src/HOL/IOA/IOA.thy
--- a/src/HOL/IOA/IOA.thy	Wed May 07 10:56:58 2008 +0200
+++ b/src/HOL/IOA/IOA.thy	Wed May 07 10:57:19 2008 +0200
@@ -337,7 +337,7 @@
 lemma externals_of_par: "externals(asig_of(A1||A2)) =
    (externals(asig_of(A1)) Un externals(asig_of(A2)))"
   apply (simp add: externals_def asig_of_par asig_comp_def
-    asig_inputs_def asig_outputs_def Un_def set_diff_def)
+    asig_inputs_def asig_outputs_def Un_def set_diff_eq)
   apply blast
   done
 
diff -r 27941d7d9a11 -r 40b411ec05aa src/HOL/Induct/Com.thy
--- a/src/HOL/Induct/Com.thy	Wed May 07 10:56:58 2008 +0200
+++ b/src/HOL/Induct/Com.thy	Wed May 07 10:57:19 2008 +0200
@@ -85,11 +85,11 @@
 
 lemma [pred_set_conv]:
   "((\<lambda>x x' y y'. ((x, x'), (y, y')) \<in> R) <= (\<lambda>x x' y y'. ((x, x'), (y, y')) \<in> S)) = (R <= S)"
-  by (auto simp add: le_fun_def le_bool_def)
+  by (auto simp add: le_fun_def le_bool_def mem_def)
 
 lemma [pred_set_conv]:
   "((\<lambda>x x' y. ((x, x'), y) \<in> R) <= (\<lambda>x x' y. ((x, x'), y) \<in> S)) = (R <= S)"
-  by (auto simp add: le_fun_def le_bool_def)
+  by (auto simp add: le_fun_def le_bool_def mem_def)
 
 declare [[unify_trace_bound = 30, unify_search_bound = 60]]
 
diff -r 27941d7d9a11 -r 40b411ec05aa src/HOL/Lambda/InductTermi.thy
--- a/src/HOL/Lambda/InductTermi.thy	Wed May 07 10:56:58 2008 +0200
+++ b/src/HOL/Lambda/InductTermi.thy	Wed May 07 10:57:19 2008 +0200
@@ -34,7 +34,6 @@
   apply clarify
   apply (rule accp.accI)
   apply (safe elim!: apps_betasE)
-     apply assumption
     apply (blast intro: subst_preserves_beta apps_preserves_beta)
    apply (blast intro: apps_preserves_beta2 subst_preserves_beta2 rtranclp_converseI
      dest: accp_downwards)  (* FIXME: acc_downwards can be replaced by acc(R ^* ) = acc(r) *)
@@ -44,7 +43,7 @@
 lemma IT_implies_termi: "IT t ==> termip beta t"
   apply (induct set: IT)
     apply (drule rev_predicate1D [OF _ listsp_mono [where B="termip beta"]])
-    apply fast
+    apply (fast intro!: predicate1I)
     apply (drule lists_accD)
     apply (erule accp_induct)
     apply (rule accp.accI)
diff -r 27941d7d9a11 -r 40b411ec05aa src/HOL/Library/Order_Relation.thy
--- a/src/HOL/Library/Order_Relation.thy	Wed May 07 10:56:58 2008 +0200
+++ b/src/HOL/Library/Order_Relation.thy	Wed May 07 10:57:19 2008 +0200
@@ -103,7 +103,7 @@
 lemma subset_Image_Image_iff:
   "\<lbrakk> Preorder r; A \<subseteq> Field r; B \<subseteq> Field r\<rbrakk> \<Longrightarrow>
    r `` A \<subseteq> r `` B \<longleftrightarrow> (\<forall>a\<in>A.\<exists>b\<in>B. (b,a):r)"
-apply(auto simp add:subset_def preorder_on_def refl_def Image_def)
+apply(auto simp add: subset_eq preorder_on_def refl_def Image_def)
 apply metis
 by(metis trans_def)
 
diff -r 27941d7d9a11 -r 40b411ec05aa src/HOL/Library/RType.thy
--- a/src/HOL/Library/RType.thy	Wed May 07 10:56:58 2008 +0200
+++ b/src/HOL/Library/RType.thy	Wed May 07 10:57:19 2008 +0200
@@ -87,7 +87,6 @@
   #> RType.add_def @{type_name fun}
   #> RType.add_def @{type_name itself}
   #> RType.add_def @{type_name bool}
-  #> RType.add_def @{type_name set}
   #> TypedefPackage.interpretation RType.perhaps_add_def
 *}
 
diff -r 27941d7d9a11 -r 40b411ec05aa src/HOL/Library/Zorn.thy
--- a/src/HOL/Library/Zorn.thy	Wed May 07 10:56:58 2008 +0200
+++ b/src/HOL/Library/Zorn.thy	Wed May 07 10:57:19 2008 +0200
@@ -44,7 +44,6 @@
   where
     succI:        "x \<in> TFin S ==> succ S x \<in> TFin S"
   | Pow_UnionI:   "Y \<in> Pow(TFin S) ==> Union(Y) \<in> TFin S"
-  monos          Pow_mono
 
 
 subsection{*Mathematical Preamble*}
@@ -57,22 +56,20 @@
 text{*This is theorem @{text increasingD2} of ZF/Zorn.thy*}
 
 lemma Abrial_axiom1: "x \<subseteq> succ S x"
-  apply (unfold succ_def)
-  apply (rule split_if [THEN iffD2])
-  apply (auto simp add: super_def maxchain_def psubset_def)
+  apply (auto simp add: succ_def super_def maxchain_def)
   apply (rule contrapos_np, assumption)
-  apply (rule someI2, blast+)
+  apply (rule_tac Q="\<lambda>S. xa \<in> S" in someI2, blast+)
   done
 
 lemmas TFin_UnionI = TFin.Pow_UnionI [OF PowI]
 
 lemma TFin_induct:
-          "[| n \<in> TFin S;
-             !!x. [| x \<in> TFin S; P(x) |] ==> P(succ S x);
-             !!Y. [| Y \<subseteq> TFin S; Ball Y P |] ==> P(Union Y) |]
-          ==> P(n)"
-  apply (induct set: TFin)
-   apply blast+
+  assumes H: "n \<in> TFin S"
+  and I: "!!x. x \<in> TFin S ==> P x ==> P (succ S x)"
+    "!!Y. Y \<subseteq> TFin S ==> Ball Y P ==> P(Union Y)"
+  shows "P n" using H
+  apply (induct rule: TFin.induct [where P=P])
+   apply (blast intro: I)+
   done
 
 lemma succ_trans: "x \<subseteq> y ==> x \<subseteq> succ S y"
@@ -163,14 +160,14 @@
 lemma select_super:
      "c \<in> chain S - maxchain S ==> (\<some>c'. c': super S c): super S c"
   apply (erule mem_super_Ex [THEN exE])
-  apply (rule someI2, auto)
+  apply (rule someI2 [where Q="%X. X : super S c"], auto)
   done
 
 lemma select_not_equals:
      "c \<in> chain S - maxchain S ==> (\<some>c'. c': super S c) \<noteq> c"
   apply (rule notI)
   apply (drule select_super)
-  apply (simp add: super_def psubset_def)
+  apply (simp add: super_def less_le)
   done
 
 lemma succI3: "c \<in> chain S - maxchain S ==> succ S c = (\<some>c'. c': super S c)"
@@ -189,7 +186,7 @@
   apply (rule CollectI, safe)
    apply (drule bspec, assumption)
    apply (rule_tac [2] m1 = Xa and n1 = X in TFin_subset_linear [THEN disjE],
-     blast+)
+     best+)
   done
 
 theorem Hausdorff: "\<exists>c. (c :: 'a set set): maxchain S"
@@ -223,7 +220,7 @@
 apply (erule conjE)
 apply (subgoal_tac "({u} Un c) \<in> super S c")
  apply simp
-apply (unfold super_def psubset_def)
+apply (unfold super_def less_le)
 apply (blast intro: chain_extend dest: chain_Union_upper)
 done
 
@@ -253,7 +250,7 @@
 apply (rule ccontr)
 apply (frule_tac z = x in chain_extend)
   apply (assumption, blast)
-apply (unfold maxchain_def super_def psubset_def)
+apply (unfold maxchain_def super_def less_le)
 apply (blast elim!: equalityCE)
 done
 
diff -r 27941d7d9a11 -r 40b411ec05aa src/HOL/MetisExamples/Tarski.thy
--- a/src/HOL/MetisExamples/Tarski.thy	Wed May 07 10:56:58 2008 +0200
+++ b/src/HOL/MetisExamples/Tarski.thy	Wed May 07 10:57:19 2008 +0200
@@ -672,7 +672,7 @@
   declare (in CLF) rel_imp_elem[intro] 
   declare interval_def [simp]
 lemma (in CLF) interval_subset: "[| a \<in> A; b \<in> A |] ==> interval r a b \<subseteq> A"
-by (metis CO_refl interval_imp_mem reflD reflD2 rel_imp_elem subset_def)
+by (metis CO_refl interval_imp_mem reflD reflD2 rel_imp_elem subset_eq)
   declare (in CLF) rel_imp_elem[rule del] 
   declare interval_def [simp del]
 
@@ -1013,7 +1013,7 @@
 ML_command{*ResAtp.problem_name:="Tarski__fz_in_int_rel"*}  (*ALL THEOREMS*)
 lemma (in Tarski) f'z_in_int_rel: "[| z \<in> P; \<forall>y\<in>Y. (y, z) \<in> induced P r |]
       ==> ((%x: intY1. f x) z, z) \<in> induced intY1 r" 
-apply (metis P_def acc_def fix_imp_eq fix_subset indI reflE restrict_apply subset_def z_in_interval)
+apply (metis P_def acc_def fix_imp_eq fix_subset indI reflE restrict_apply subset_eq z_in_interval)
 done
 
 (*never proved, 2007-01-22*)
diff -r 27941d7d9a11 -r 40b411ec05aa src/HOL/MetisExamples/set.thy
--- a/src/HOL/MetisExamples/set.thy	Wed May 07 10:56:58 2008 +0200
+++ b/src/HOL/MetisExamples/set.thy	Wed May 07 10:57:19 2008 +0200
@@ -238,7 +238,7 @@
 
 lemma (*singleton_example_2:*)
      "\<forall>x \<in> S. \<Union>S \<subseteq> x \<Longrightarrow> \<exists>z. S \<subseteq> {z}"
-by (metis Un_absorb2 Union_insert insertI1 insert_Diff insert_Diff_single subset_def)
+by (metis Un_absorb2 Union_insert insertI1 insert_Diff insert_Diff_single subset_eq)
 
 lemma singleton_example_2:
      "\<forall>x \<in> S. \<Union>S \<subseteq> x \<Longrightarrow> \<exists>z. S \<subseteq> {z}"
diff -r 27941d7d9a11 -r 40b411ec05aa src/HOL/MicroJava/BV/Listn.thy
--- a/src/HOL/MicroJava/BV/Listn.thy	Wed May 07 10:56:58 2008 +0200
+++ b/src/HOL/MicroJava/BV/Listn.thy	Wed May 07 10:57:19 2008 +0200
@@ -330,7 +330,7 @@
  apply (rename_tac m n)
  apply (case_tac "m=n")
   apply simp
- apply (fast intro!: equals0I [to_pred bot_empty_eq] dest: not_sym)
+ apply (fast intro!: equals0I [to_pred bot_empty_eq pred_equals_eq] dest: not_sym)
 apply clarify
 apply (rename_tac n)
 apply (induct_tac n)
diff -r 27941d7d9a11 -r 40b411ec05aa src/HOL/Nominal/Examples/Class.thy
--- a/src/HOL/Nominal/Examples/Class.thy	Wed May 07 10:56:58 2008 +0200
+++ b/src/HOL/Nominal/Examples/Class.thy	Wed May 07 10:57:19 2008 +0200
@@ -10317,7 +10317,7 @@
 lemma NOTRIGHT_eqvt_name:
   fixes pi::"name prm"
   shows "(pi\<bullet>(NOTRIGHT (NOT B) X)) = NOTRIGHT (NOT B) (pi\<bullet>X)"
-apply(auto simp add: perm_set_def)
+apply(auto simp add: perm_set_eq)
 apply(rule_tac x="pi\<bullet>a" in exI) 
 apply(rule_tac x="pi\<bullet>xb" in exI) 
 apply(rule_tac x="pi\<bullet>M" in exI)
@@ -10343,7 +10343,7 @@
 lemma NOTRIGHT_eqvt_coname:
   fixes pi::"coname prm"
   shows "(pi\<bullet>(NOTRIGHT (NOT B) X)) = NOTRIGHT (NOT B) (pi\<bullet>X)"
-apply(auto simp add: perm_set_def)
+apply(auto simp add: perm_set_eq)
 apply(rule_tac x="pi\<bullet>a" in exI) 
 apply(rule_tac x="pi\<bullet>xb" in exI) 
 apply(rule_tac x="pi\<bullet>M" in exI)
@@ -10377,7 +10377,7 @@
 lemma NOTLEFT_eqvt_name:
   fixes pi::"name prm"
   shows "(pi\<bullet>(NOTLEFT (NOT B) X)) = NOTLEFT (NOT B) (pi\<bullet>X)"
-apply(auto simp add: perm_set_def)
+apply(auto simp add: perm_set_eq)
 apply(rule_tac x="pi\<bullet>a" in exI) 
 apply(rule_tac x="pi\<bullet>xb" in exI) 
 apply(rule_tac x="pi\<bullet>M" in exI)
@@ -10403,7 +10403,7 @@
 lemma NOTLEFT_eqvt_coname:
   fixes pi::"coname prm"
   shows "(pi\<bullet>(NOTLEFT (NOT B) X)) = NOTLEFT (NOT B) (pi\<bullet>X)"
-apply(auto simp add: perm_set_def)
+apply(auto simp add: perm_set_eq)
 apply(rule_tac x="pi\<bullet>a" in exI) 
 apply(rule_tac x="pi\<bullet>xb" in exI) 
 apply(rule_tac x="pi\<bullet>M" in exI)
@@ -10438,7 +10438,7 @@
 lemma ANDRIGHT_eqvt_name:
   fixes pi::"name prm"
   shows "(pi\<bullet>(ANDRIGHT (A AND B) X Y)) = ANDRIGHT (A AND B) (pi\<bullet>X) (pi\<bullet>Y)"
-apply(auto simp add: perm_set_def)
+apply(auto simp add: perm_set_eq)
 apply(rule_tac x="pi\<bullet>c" in exI)
 apply(rule_tac x="pi\<bullet>a" in exI)
 apply(rule_tac x="pi\<bullet>b" in exI)
@@ -10473,7 +10473,7 @@
 lemma ANDRIGHT_eqvt_coname:
   fixes pi::"coname prm"
   shows "(pi\<bullet>(ANDRIGHT (A AND B) X Y)) = ANDRIGHT (A AND B) (pi\<bullet>X) (pi\<bullet>Y)"
-apply(auto simp add: perm_set_def)
+apply(auto simp add: perm_set_eq)
 apply(rule_tac x="pi\<bullet>c" in exI)
 apply(rule_tac x="pi\<bullet>a" in exI)
 apply(rule_tac x="pi\<bullet>b" in exI)
@@ -10516,7 +10516,7 @@
 lemma ANDLEFT1_eqvt_name:
   fixes pi::"name prm"
   shows "(pi\<bullet>(ANDLEFT1 (A AND B) X)) = ANDLEFT1 (A AND B) (pi\<bullet>X)"
-apply(auto simp add: perm_set_def)
+apply(auto simp add: perm_set_eq)
 apply(rule_tac x="pi\<bullet>xb" in exI) 
 apply(rule_tac x="pi\<bullet>y" in exI) 
 apply(rule_tac x="pi\<bullet>M" in exI)
@@ -10542,7 +10542,7 @@
 lemma ANDLEFT1_eqvt_coname:
   fixes pi::"coname prm"
   shows "(pi\<bullet>(ANDLEFT1 (A AND B) X)) = ANDLEFT1 (A AND B) (pi\<bullet>X)"
-apply(auto simp add: perm_set_def)
+apply(auto simp add: perm_set_eq)
 apply(rule_tac x="pi\<bullet>xb" in exI) 
 apply(rule_tac x="pi\<bullet>y" in exI) 
 apply(rule_tac x="pi\<bullet>M" in exI)
@@ -10576,7 +10576,7 @@
 lemma ANDLEFT2_eqvt_name:
   fixes pi::"name prm"
   shows "(pi\<bullet>(ANDLEFT2 (A AND B) X)) = ANDLEFT2 (A AND B) (pi\<bullet>X)"
-apply(auto simp add: perm_set_def)
+apply(auto simp add: perm_set_eq)
 apply(rule_tac x="pi\<bullet>xb" in exI) 
 apply(rule_tac x="pi\<bullet>y" in exI) 
 apply(rule_tac x="pi\<bullet>M" in exI)
@@ -10602,7 +10602,7 @@
 lemma ANDLEFT2_eqvt_coname:
   fixes pi::"coname prm"
   shows "(pi\<bullet>(ANDLEFT2 (A AND B) X)) = ANDLEFT2 (A AND B) (pi\<bullet>X)"
-apply(auto simp add: perm_set_def)
+apply(auto simp add: perm_set_eq)
 apply(rule_tac x="pi\<bullet>xb" in exI) 
 apply(rule_tac x="pi\<bullet>y" in exI) 
 apply(rule_tac x="pi\<bullet>M" in exI)
@@ -10637,7 +10637,7 @@
 lemma ORLEFT_eqvt_name:
   fixes pi::"name prm"
   shows "(pi\<bullet>(ORLEFT (A OR B) X Y)) = ORLEFT (A OR B) (pi\<bullet>X) (pi\<bullet>Y)"
-apply(auto simp add: perm_set_def)
+apply(auto simp add: perm_set_eq)
 apply(rule_tac x="pi\<bullet>xb" in exI)
 apply(rule_tac x="pi\<bullet>y" in exI)
 apply(rule_tac x="pi\<bullet>z" in exI)
@@ -10672,7 +10672,7 @@
 lemma ORLEFT_eqvt_coname:
   fixes pi::"coname prm"
   shows "(pi\<bullet>(ORLEFT (A OR B) X Y)) = ORLEFT (A OR B) (pi\<bullet>X) (pi\<bullet>Y)"
-apply(auto simp add: perm_set_def)
+apply(auto simp add: perm_set_eq)
 apply(rule_tac x="pi\<bullet>xb" in exI)
 apply(rule_tac x="pi\<bullet>y" in exI)
 apply(rule_tac x="pi\<bullet>z" in exI)
@@ -10715,7 +10715,7 @@
 lemma ORRIGHT1_eqvt_name:
   fixes pi::"name prm"
   shows "(pi\<bullet>(ORRIGHT1 (A OR B) X)) = ORRIGHT1 (A OR B) (pi\<bullet>X)"
-apply(auto simp add: perm_set_def)
+apply(auto simp add: perm_set_eq)
 apply(rule_tac x="pi\<bullet>a" in exI) 
 apply(rule_tac x="pi\<bullet>b" in exI) 
 apply(rule_tac x="pi\<bullet>M" in exI)
@@ -10741,7 +10741,7 @@
 lemma ORRIGHT1_eqvt_coname:
   fixes pi::"coname prm"
   shows "(pi\<bullet>(ORRIGHT1 (A OR B) X)) = ORRIGHT1 (A OR B) (pi\<bullet>X)"
-apply(auto simp add: perm_set_def)
+apply(auto simp add: perm_set_eq)
 apply(rule_tac x="pi\<bullet>a" in exI) 
 apply(rule_tac x="pi\<bullet>b" in exI) 
 apply(rule_tac x="pi\<bullet>M" in exI)
@@ -10775,7 +10775,7 @@
 lemma ORRIGHT2_eqvt_name:
   fixes pi::"name prm"
   shows "(pi\<bullet>(ORRIGHT2 (A OR B) X)) = ORRIGHT2 (A OR B) (pi\<bullet>X)"
-apply(auto simp add: perm_set_def)
+apply(auto simp add: perm_set_eq)
 apply(rule_tac x="pi\<bullet>a" in exI) 
 apply(rule_tac x="pi\<bullet>b" in exI) 
 apply(rule_tac x="pi\<bullet>M" in exI)
@@ -10801,7 +10801,7 @@
 lemma ORRIGHT2_eqvt_coname:
   fixes pi::"coname prm"
   shows "(pi\<bullet>(ORRIGHT2 (A OR B) X)) = ORRIGHT2 (A OR B) (pi\<bullet>X)"
-apply(auto simp add: perm_set_def)
+apply(auto simp add: perm_set_eq)
 apply(rule_tac x="pi\<bullet>a" in exI) 
 apply(rule_tac x="pi\<bullet>b" in exI) 
 apply(rule_tac x="pi\<bullet>M" in exI)
@@ -10838,7 +10838,7 @@
 lemma IMPRIGHT_eqvt_name:
   fixes pi::"name prm"
   shows "(pi\<bullet>(IMPRIGHT (A IMP B) X Y Z U)) = IMPRIGHT (A IMP B) (pi\<bullet>X) (pi\<bullet>Y) (pi\<bullet>Z) (pi\<bullet>U)"
-apply(auto simp add: perm_set_def)
+apply(auto simp add: perm_set_eq)
 apply(rule_tac x="pi\<bullet>xb" in exI)
 apply(rule_tac x="pi\<bullet>a" in exI)
 apply(rule_tac x="pi\<bullet>b" in exI)
@@ -10898,7 +10898,7 @@
 lemma IMPRIGHT_eqvt_coname:
   fixes pi::"coname prm"
   shows "(pi\<bullet>(IMPRIGHT (A IMP B) X Y Z U)) = IMPRIGHT (A IMP B) (pi\<bullet>X) (pi\<bullet>Y) (pi\<bullet>Z) (pi\<bullet>U)"
-apply(auto simp add: perm_set_def)
+apply(auto simp add: perm_set_eq)
 apply(rule_tac x="pi\<bullet>xb" in exI)
 apply(rule_tac x="pi\<bullet>a" in exI)
 apply(rule_tac x="pi\<bullet>b" in exI)
@@ -10966,7 +10966,7 @@
 lemma IMPLEFT_eqvt_name:
   fixes pi::"name prm"
   shows "(pi\<bullet>(IMPLEFT (A IMP B) X Y)) = IMPLEFT (A IMP B) (pi\<bullet>X) (pi\<bullet>Y)"
-apply(auto simp add: perm_set_def)
+apply(auto simp add: perm_set_eq)
 apply(rule_tac x="pi\<bullet>xb" in exI) 
 apply(rule_tac x="pi\<bullet>a" in exI)
 apply(rule_tac x="pi\<bullet>y" in exI) 
@@ -11001,7 +11001,7 @@
 lemma IMPLEFT_eqvt_coname:
   fixes pi::"coname prm"
   shows "(pi\<bullet>(IMPLEFT (A IMP B) X Y)) = IMPLEFT (A IMP B) (pi\<bullet>X) (pi\<bullet>Y)"
-apply(auto simp add: perm_set_def)
+apply(auto simp add: perm_set_eq)
 apply(rule_tac x="pi\<bullet>xb" in exI) 
 apply(rule_tac x="pi\<bullet>a" in exI)
 apply(rule_tac x="pi\<bullet>y" in exI) 
@@ -11098,16 +11098,6 @@
   shows "x\<in>(X\<inter>Y) = (x\<in>X \<and> x\<in>Y)"
 by blast
 
-lemma pt_Collect_eqvt:
-  fixes pi::"'x prm"
-  assumes pt: "pt TYPE('a) TYPE('x)"
-  and     at: "at TYPE('x)"
-  shows "pi\<bullet>{x::'a. P x} = {x. P ((rev pi)\<bullet>x)}"
-apply(auto simp add: perm_set_def  pt_rev_pi[OF pt, OF at])
-apply(rule_tac x="(rev pi)\<bullet>x" in exI)
-apply(simp add: pt_pi_rev[OF pt, OF at])
-done
-
 lemma big_inter_eqvt:
   fixes pi1::"name prm"
   and   X::"('a::pt_name) set set"
@@ -11115,7 +11105,7 @@
   and   Y::"('b::pt_coname) set set"
   shows "(pi1\<bullet>(\<Inter> X)) = \<Inter> (pi1\<bullet>X)"
   and   "(pi2\<bullet>(\<Inter> Y)) = \<Inter> (pi2\<bullet>Y)"
-apply(auto simp add: perm_set_def)
+apply(auto simp add: perm_set_eq)
 apply(rule_tac x="(rev pi1)\<bullet>x" in exI)
 apply(perm_simp)
 apply(rule ballI)
@@ -11150,7 +11140,7 @@
   shows "pi1\<bullet>(lfp f) = lfp (pi1\<bullet>f)"
   and   "pi2\<bullet>(lfp g) = lfp (pi2\<bullet>g)"
 apply(simp add: lfp_def)
-apply(simp add: Inf_set_def)
+apply(simp add: Inf_set_eq)
 apply(simp add: big_inter_eqvt)
 apply(simp add: pt_Collect_eqvt[OF pt_name_inst, OF at_name_inst])
 apply(subgoal_tac "{u. (pi1\<bullet>f) u \<subseteq> u} = {u. ((rev pi1)\<bullet>((pi1\<bullet>f) u)) \<subseteq> ((rev pi1)\<bullet>u)}")
@@ -11162,7 +11152,7 @@
 apply(drule subseteq_eqvt(1)[THEN iffD2])
 apply(simp add: perm_bool)
 apply(simp add: lfp_def)
-apply(simp add: Inf_set_def)
+apply(simp add: Inf_set_eq)
 apply(simp add: big_inter_eqvt)
 apply(simp add: pt_Collect_eqvt[OF pt_coname_inst, OF at_coname_inst])
 apply(subgoal_tac "{u. (pi2\<bullet>g) u \<subseteq> u} = {u. ((rev pi2)\<bullet>((pi2\<bullet>g) u)) \<subseteq> ((rev pi2)\<bullet>u)}")
@@ -11345,7 +11335,7 @@
   fixes pi::"name prm"
   shows "(pi\<bullet>(BINDINGn B X)) = BINDINGn B (pi\<bullet>X)" 
   and   "(pi\<bullet>(BINDINGc B Y)) = BINDINGc B (pi\<bullet>Y)" 
-apply(auto simp add: BINDINGn_def BINDINGc_def perm_set_def)
+apply(auto simp add: BINDINGn_def BINDINGc_def perm_set_eq)
 apply(rule_tac x="pi\<bullet>xb" in exI)
 apply(rule_tac x="pi\<bullet>M" in exI)
 apply(simp)
@@ -11400,7 +11390,7 @@
   fixes pi::"coname prm"
   shows "(pi\<bullet>(BINDINGn B X)) = BINDINGn B (pi\<bullet>X)" 
   and   "(pi\<bullet>(BINDINGc B Y)) = BINDINGc B (pi\<bullet>Y)" 
-apply(auto simp add: BINDINGn_def BINDINGc_def perm_set_def)
+apply(auto simp add: BINDINGn_def BINDINGc_def perm_set_eq)
 apply(rule_tac x="pi\<bullet>xb" in exI)
 apply(rule_tac x="pi\<bullet>M" in exI)
 apply(simp)
@@ -11460,7 +11450,7 @@
   { case 1 show ?case 
       apply -
       apply(simp add: lfp_eqvt)
-      apply(simp add: perm_fun_def)
+      apply(simp add: perm_fun_def [where 'a="ntrm \<Rightarrow> bool"])
       apply(simp add: union_eqvt AXIOMS_eqvt_name BINDING_eqvt_name)
       apply(perm_simp)
     done
@@ -11471,7 +11461,7 @@
       apply(simp add: union_eqvt AXIOMS_eqvt_name BINDING_eqvt_name)
       apply(simp add: lfp_eqvt)
       apply(simp add: comp_def)
-      apply(simp add: perm_fun_def)
+      apply(simp add: perm_fun_def [where 'a="ntrm \<Rightarrow> bool"])
       apply(simp add: union_eqvt AXIOMS_eqvt_name BINDING_eqvt_name)
       apply(perm_simp)
       done
@@ -11484,7 +11474,7 @@
     apply -
     apply(simp only: lfp_eqvt)
     apply(simp only: comp_def)
-    apply(simp only: perm_fun_def)
+    apply(simp only: perm_fun_def [where 'a="ntrm \<Rightarrow> bool"])
     apply(simp only: NEGc.simps NEGn.simps)
     apply(simp only: union_eqvt AXIOMS_eqvt_name BINDING_eqvt_name NOTRIGHT_eqvt_name NOTLEFT_eqvt_name)
     apply(perm_simp add: ih1 ih2)
@@ -11504,7 +11494,7 @@
     apply -
     apply(simp only: lfp_eqvt)
     apply(simp only: comp_def)
-    apply(simp only: perm_fun_def)
+    apply(simp only: perm_fun_def [where 'a="ntrm \<Rightarrow> bool"])
     apply(simp only: NEGc.simps NEGn.simps)
     apply(simp only: union_eqvt AXIOMS_eqvt_name BINDING_eqvt_name ANDRIGHT_eqvt_name 
                      ANDLEFT2_eqvt_name ANDLEFT1_eqvt_name)
@@ -11526,7 +11516,7 @@
     apply -
     apply(simp only: lfp_eqvt)
     apply(simp only: comp_def)
-    apply(simp only: perm_fun_def)
+    apply(simp only: perm_fun_def [where 'a="ntrm \<Rightarrow> bool"])
     apply(simp only: NEGc.simps NEGn.simps)
     apply(simp only: union_eqvt AXIOMS_eqvt_name BINDING_eqvt_name ORRIGHT1_eqvt_name 
                      ORRIGHT2_eqvt_name ORLEFT_eqvt_name)
@@ -11548,7 +11538,7 @@
     apply -
     apply(simp only: lfp_eqvt)
     apply(simp only: comp_def)
-    apply(simp only: perm_fun_def)
+    apply(simp only: perm_fun_def [where 'a="ntrm \<Rightarrow> bool"])
     apply(simp only: NEGc.simps NEGn.simps)
     apply(simp only: union_eqvt AXIOMS_eqvt_name BINDING_eqvt_name IMPRIGHT_eqvt_name IMPLEFT_eqvt_name)
     apply(perm_simp add: ih1 ih2 ih3 ih4)
@@ -11570,7 +11560,7 @@
   { case 1 show ?case 
       apply -
       apply(simp add: lfp_eqvt)
-      apply(simp add: perm_fun_def)
+      apply(simp add: perm_fun_def [where 'a="ntrm \<Rightarrow> bool"])
       apply(simp add: union_eqvt AXIOMS_eqvt_coname BINDING_eqvt_coname)
       apply(perm_simp)
     done
@@ -11581,7 +11571,7 @@
       apply(simp add: union_eqvt AXIOMS_eqvt_coname BINDING_eqvt_coname)
       apply(simp add: lfp_eqvt)
       apply(simp add: comp_def)
-      apply(simp add: perm_fun_def)
+      apply(simp add: perm_fun_def [where 'a="ntrm \<Rightarrow> bool"])
       apply(simp add: union_eqvt AXIOMS_eqvt_coname BINDING_eqvt_coname)
       apply(perm_simp)
       done
@@ -11594,7 +11584,7 @@
     apply -
     apply(simp only: lfp_eqvt)
     apply(simp only: comp_def)
-    apply(simp only: perm_fun_def)
+    apply(simp only: perm_fun_def [where 'a="ntrm \<Rightarrow> bool"])
     apply(simp only: NEGc.simps NEGn.simps)
     apply(simp only: union_eqvt AXIOMS_eqvt_coname BINDING_eqvt_coname 
             NOTRIGHT_eqvt_coname NOTLEFT_eqvt_coname)
@@ -11616,7 +11606,7 @@
     apply -
     apply(simp only: lfp_eqvt)
     apply(simp only: comp_def)
-    apply(simp only: perm_fun_def)
+    apply(simp only: perm_fun_def [where 'a="ntrm \<Rightarrow> bool"])
     apply(simp only: NEGc.simps NEGn.simps)
     apply(simp only: union_eqvt AXIOMS_eqvt_coname BINDING_eqvt_coname ANDRIGHT_eqvt_coname 
                      ANDLEFT2_eqvt_coname ANDLEFT1_eqvt_coname)
@@ -11638,7 +11628,7 @@
     apply -
     apply(simp only: lfp_eqvt)
     apply(simp only: comp_def)
-    apply(simp only: perm_fun_def)
+    apply(simp only: perm_fun_def [where 'a="ntrm \<Rightarrow> bool"])
     apply(simp only: NEGc.simps NEGn.simps)
     apply(simp only: union_eqvt AXIOMS_eqvt_coname BINDING_eqvt_coname ORRIGHT1_eqvt_coname 
                      ORRIGHT2_eqvt_coname ORLEFT_eqvt_coname)
@@ -11660,7 +11650,7 @@
     apply -
     apply(simp only: lfp_eqvt)
     apply(simp only: comp_def)
-    apply(simp only: perm_fun_def)
+    apply(simp only: perm_fun_def [where 'a="ntrm \<Rightarrow> bool"])
     apply(simp only: NEGc.simps NEGn.simps)
     apply(simp only: union_eqvt AXIOMS_eqvt_coname BINDING_eqvt_coname IMPRIGHT_eqvt_coname 
          IMPLEFT_eqvt_coname)
diff -r 27941d7d9a11 -r 40b411ec05aa src/HOL/Nominal/Examples/SOS.thy
--- a/src/HOL/Nominal/Examples/SOS.thy	Wed May 07 10:56:58 2008 +0200
+++ b/src/HOL/Nominal/Examples/SOS.thy	Wed May 07 10:57:19 2008 +0200
@@ -422,7 +422,7 @@
   shows "(pi\<bullet>x)\<in>V T"
 using a
 apply(nominal_induct T arbitrary: pi x rule: ty.induct)
-apply(auto simp add: trm.inject perm_set_def)
+apply(auto simp add: trm.inject)
 apply(simp add: eqvts)
 apply(rule_tac x="pi\<bullet>xa" in exI)
 apply(rule_tac x="pi\<bullet>e" in exI)
diff -r 27941d7d9a11 -r 40b411ec05aa src/HOL/Nominal/Examples/Support.thy
--- a/src/HOL/Nominal/Examples/Support.thy	Wed May 07 10:56:58 2008 +0200
+++ b/src/HOL/Nominal/Examples/Support.thy	Wed May 07 10:57:19 2008 +0200
@@ -100,14 +100,14 @@
     proof (cases "x\<in>S")
       case True
       have "x\<in>S" by fact
-      hence "\<forall>b\<in>(UNIV-S). [(x,b)]\<bullet>S\<noteq>S" by (auto simp add: perm_set_def calc_atm)
+      hence "\<forall>b\<in>(UNIV-S). [(x,b)]\<bullet>S\<noteq>S" by (auto simp add: perm_set_eq calc_atm)
       with asm2 have "infinite {b\<in>(UNIV-S). [(x,b)]\<bullet>S\<noteq>S}" by (rule infinite_Collection)
       hence "infinite {b. [(x,b)]\<bullet>S\<noteq>S}" by (rule_tac infinite_super, auto)
       then show "x\<in>(supp S)" by (simp add: supp_def)
     next
       case False
       have "x\<notin>S" by fact
-      hence "\<forall>b\<in>S. [(x,b)]\<bullet>S\<noteq>S" by (auto simp add: perm_set_def calc_atm)
+      hence "\<forall>b\<in>S. [(x,b)]\<bullet>S\<noteq>S" by (auto simp add: perm_set_eq calc_atm)
       with asm1 have "infinite {b\<in>S. [(x,b)]\<bullet>S\<noteq>S}" by (rule infinite_Collection)
       hence "infinite {b. [(x,b)]\<bullet>S\<noteq>S}" by (rule_tac infinite_super, auto)
       then show "x\<in>(supp S)" by (simp add: supp_def)
@@ -131,7 +131,7 @@
   shows "supp (UNIV::atom set) = ({}::atom set)"
 proof -
   have "\<forall>(x::atom) (y::atom). [(x,y)]\<bullet>UNIV = (UNIV::atom set)"
-    by (auto simp add: perm_set_def calc_atm)
+    by (auto simp add: perm_set_eq calc_atm)
   then show "supp (UNIV::atom set) = ({}::atom set)" by (simp add: supp_def)
 qed
 
diff -r 27941d7d9a11 -r 40b411ec05aa src/HOL/Nominal/Nominal.thy
--- a/src/HOL/Nominal/Nominal.thy	Wed May 07 10:56:58 2008 +0200
+++ b/src/HOL/Nominal/Nominal.thy	Wed May 07 10:57:19 2008 +0200
@@ -29,61 +29,6 @@
 constdefs
   "perm_aux pi x \<equiv> pi\<bullet>x"
 
-(* permutation on sets *)
-defs (unchecked overloaded)
-  perm_set_def:  "pi\<bullet>(X::'a set) \<equiv> {pi\<bullet>x | x. x\<in>X}"
-
-lemma empty_eqvt:
-  shows "pi\<bullet>{} = {}"
-  by (simp add: perm_set_def)
-
-lemma union_eqvt:
-  shows "(pi\<bullet>(X\<union>Y)) = (pi\<bullet>X) \<union> (pi\<bullet>Y)"
-  by (auto simp add: perm_set_def)
-
-lemma insert_eqvt:
-  shows "pi\<bullet>(insert x X) = insert (pi\<bullet>x) (pi\<bullet>X)"
-  by (auto simp add: perm_set_def)
-
-(* permutation on units and products *)
-primrec (unchecked perm_unit)
-  "pi\<bullet>() = ()"
-  
-primrec (unchecked perm_prod)
-  "pi\<bullet>(x,y) = (pi\<bullet>x,pi\<bullet>y)"
-
-lemma fst_eqvt:
-  "pi\<bullet>(fst x) = fst (pi\<bullet>x)"
- by (cases x) simp
-
-lemma snd_eqvt:
-  "pi\<bullet>(snd x) = snd (pi\<bullet>x)"
- by (cases x) simp
-
-(* permutation on lists *)
-primrec (unchecked perm_list)
-  nil_eqvt:  "pi\<bullet>[]     = []"
-  cons_eqvt: "pi\<bullet>(x#xs) = (pi\<bullet>x)#(pi\<bullet>xs)"
-
-lemma append_eqvt:
-  fixes pi :: "'x prm"
-  and   l1 :: "'a list"
-  and   l2 :: "'a list"
-  shows "pi\<bullet>(l1@l2) = (pi\<bullet>l1)@(pi\<bullet>l2)"
-  by (induct l1) auto
-
-lemma rev_eqvt:
-  fixes pi :: "'x prm"
-  and   l  :: "'a list"
-  shows "pi\<bullet>(rev l) = rev (pi\<bullet>l)"
-  by (induct l) (simp_all add: append_eqvt)
-
-lemma set_eqvt:
-  fixes pi :: "'x prm"
-  and   xs :: "'a list"
-  shows "pi\<bullet>(set xs) = set (pi\<bullet>xs)"
-by (induct xs) (auto simp add: empty_eqvt insert_eqvt)
-
 (* permutation on functions *)
 defs (unchecked overloaded)
   perm_fun_def: "pi\<bullet>(f::'a\<Rightarrow>'b) \<equiv> (\<lambda>x. pi\<bullet>f((rev pi)\<bullet>x))"
@@ -129,6 +74,48 @@
   shows "pi\<bullet>(\<not> A) = (\<not> (pi\<bullet>A))"
   by (simp add: perm_bool)
 
+(* permutation on sets *)
+lemma empty_eqvt:
+  shows "pi\<bullet>{} = {}"
+  by (simp add: perm_fun_def perm_bool empty_iff [unfolded mem_def] expand_fun_eq)
+
+lemma union_eqvt:
+  shows "(pi\<bullet>(X\<union>Y)) = (pi\<bullet>X) \<union> (pi\<bullet>Y)"
+  by (simp add: perm_fun_def perm_bool Un_iff [unfolded mem_def] expand_fun_eq)
+
+(* permutation on units and products *)
+primrec (unchecked perm_unit)
+  "pi\<bullet>() = ()"
+  
+primrec (unchecked perm_prod)
+  "pi\<bullet>(x,y) = (pi\<bullet>x,pi\<bullet>y)"
+
+lemma fst_eqvt:
+  "pi\<bullet>(fst x) = fst (pi\<bullet>x)"
+ by (cases x) simp
+
+lemma snd_eqvt:
+  "pi\<bullet>(snd x) = snd (pi\<bullet>x)"
+ by (cases x) simp
+
+(* permutation on lists *)
+primrec (unchecked perm_list)
+  nil_eqvt:  "pi\<bullet>[]     = []"
+  cons_eqvt: "pi\<bullet>(x#xs) = (pi\<bullet>x)#(pi\<bullet>xs)"
+
+lemma append_eqvt:
+  fixes pi :: "'x prm"
+  and   l1 :: "'a list"
+  and   l2 :: "'a list"
+  shows "pi\<bullet>(l1@l2) = (pi\<bullet>l1)@(pi\<bullet>l2)"
+  by (induct l1) auto
+
+lemma rev_eqvt:
+  fixes pi :: "'x prm"
+  and   l  :: "'a list"
+  shows "pi\<bullet>(rev l) = rev (pi\<bullet>l)"
+  by (induct l) (simp_all add: append_eqvt)
+
 (* permutation on options *)
 
 primrec (unchecked perm_option)
@@ -196,11 +183,7 @@
 
 lemma supp_set_empty:
   shows "supp {} = {}"
-  by (force simp add: supp_def perm_set_def)
-
-lemma supp_singleton:
-  shows "supp {x} = supp x"
-  by (force simp add: supp_def perm_set_def)
+  by (force simp add: supp_def empty_eqvt)
 
 lemma supp_prod: 
   fixes x :: "'a"
@@ -284,10 +267,6 @@
   shows "a\<sharp>{}"
   by (simp add: fresh_def supp_set_empty)
 
-lemma fresh_singleton:
-  shows "a\<sharp>{x} = a\<sharp>x"
-  by (simp add: fresh_def supp_singleton)
-
 lemma fresh_unit:
   shows "a\<sharp>()"
   by (simp add: fresh_def supp_unit)
@@ -1026,15 +1005,6 @@
 section {* permutation type instances *}
 (* ===================================*)
 
-lemma pt_set_inst:
-  assumes pt: "pt TYPE('a) TYPE('x)"
-  shows  "pt TYPE('a set) TYPE('x)"
-apply(simp add: pt_def)
-apply(simp_all add: perm_set_def)
-apply(simp add: pt1[OF pt])
-apply(force simp add: pt2[OF pt] pt3[OF pt])
-done
-
 lemma pt_list_nil: 
   fixes xs :: "'a list"
   assumes pt: "pt TYPE('a) TYPE ('x)"
@@ -1270,6 +1240,42 @@
 apply(rule pt1[OF pt])
 done
 
+lemma perm_set_eq:
+  assumes pt: "pt TYPE('a) TYPE('x)"
+  and at: "at TYPE('x)" 
+  shows "(pi::'x prm)\<bullet>(X::'a set) = {pi\<bullet>x | x. x\<in>X}"
+  apply (auto simp add: perm_fun_def perm_bool mem_def)
+  apply (rule_tac x="rev pi \<bullet> x" in exI)
+  apply (simp add: pt_pi_rev [OF pt at])
+  apply (simp add: pt_rev_pi [OF pt at])
+  done
+
+lemma insert_eqvt:
+  assumes pt: "pt TYPE('a) TYPE('x)"
+  and at: "at TYPE('x)" 
+  shows "(pi::'x prm)\<bullet>(insert (x::'a) X) = insert (pi\<bullet>x) (pi\<bullet>X)"
+  by (auto simp add: perm_set_eq [OF pt at])
+
+lemma set_eqvt:
+  fixes pi :: "'x prm"
+  and   xs :: "'a list"
+  assumes pt: "pt TYPE('a) TYPE('x)"
+  and at: "at TYPE('x)" 
+  shows "pi\<bullet>(set xs) = set (pi\<bullet>xs)"
+by (induct xs) (auto simp add: empty_eqvt insert_eqvt [OF pt at])
+
+lemma supp_singleton:
+  assumes pt: "pt TYPE('a) TYPE('x)"
+  and at: "at TYPE('x)" 
+  shows "(supp {x::'a} :: 'x set) = supp x"
+  by (force simp add: supp_def perm_set_eq [OF pt at])
+
+lemma fresh_singleton:
+  assumes pt: "pt TYPE('a) TYPE('x)"
+  and at: "at TYPE('x)" 
+  shows "(a::'x)\<sharp>{x::'a} = a\<sharp>x"
+  by (simp add: fresh_def supp_singleton [OF pt at])
+
 lemma pt_set_bij1:
   fixes pi :: "'x prm"
   and   x  :: "'a"
@@ -1277,7 +1283,7 @@
   assumes pt: "pt TYPE('a) TYPE('x)"
   and     at: "at TYPE('x)"
   shows "((pi\<bullet>x)\<in>X) = (x\<in>((rev pi)\<bullet>X))"
-  by (force simp add: perm_set_def pt_rev_pi[OF pt, OF at] pt_pi_rev[OF pt, OF at])
+  by (force simp add: perm_set_eq [OF pt at] pt_rev_pi[OF pt, OF at] pt_pi_rev[OF pt, OF at])
 
 lemma pt_set_bij1a:
   fixes pi :: "'x prm"
@@ -1286,7 +1292,7 @@
   assumes pt: "pt TYPE('a) TYPE('x)"
   and     at: "at TYPE('x)"
   shows "(x\<in>(pi\<bullet>X)) = (((rev pi)\<bullet>x)\<in>X)"
-  by (force simp add: perm_set_def pt_rev_pi[OF pt, OF at] pt_pi_rev[OF pt, OF at])
+  by (force simp add: perm_set_eq [OF pt at] pt_rev_pi[OF pt, OF at] pt_pi_rev[OF pt, OF at])
 
 lemma pt_set_bij:
   fixes pi :: "'x prm"
@@ -1295,7 +1301,7 @@
   assumes pt: "pt TYPE('a) TYPE('x)"
   and     at: "at TYPE('x)"
   shows "((pi\<bullet>x)\<in>(pi\<bullet>X)) = (x\<in>X)"
-  by (simp add: perm_set_def pt_bij[OF pt, OF at])
+  by (simp add: perm_set_eq [OF pt at] pt_bij[OF pt, OF at])
 
 lemma pt_in_eqvt:
   fixes pi :: "'x prm"
@@ -1342,7 +1348,7 @@
   assumes pt: "pt TYPE('a) TYPE('x)"
   and     at: "at TYPE('x)"
   shows "(pi\<bullet>(X\<subseteq>Y)) = ((pi\<bullet>X)\<subseteq>(pi\<bullet>Y))"
-by (auto simp add: perm_set_def perm_bool pt_bij[OF pt, OF at])
+by (auto simp add: perm_set_eq [OF pt at] perm_bool pt_bij[OF pt, OF at])
 
 lemma pt_set_diff_eqvt:
   fixes X::"'a set"
@@ -1351,14 +1357,14 @@
   assumes pt: "pt TYPE('a) TYPE('x)"
   and     at: "at TYPE('x)"
   shows "pi\<bullet>(X - Y) = (pi\<bullet>X) - (pi\<bullet>Y)"
-  by (auto simp add: perm_set_def pt_bij[OF pt, OF at])
+  by (auto simp add: perm_set_eq [OF pt at] pt_bij[OF pt, OF at])
 
 lemma pt_Collect_eqvt:
   fixes pi::"'x prm"
   assumes pt: "pt TYPE('a) TYPE('x)"
   and     at: "at TYPE('x)"
   shows "pi\<bullet>{x::'a. P x} = {x. P ((rev pi)\<bullet>x)}"
-apply(auto simp add: perm_set_def  pt_rev_pi[OF pt, OF at])
+apply(auto simp add: perm_set_eq [OF pt at] pt_rev_pi[OF pt, OF at])
 apply(rule_tac x="(rev pi)\<bullet>x" in exI)
 apply(simp add: pt_pi_rev[OF pt, OF at])
 done
@@ -1402,7 +1408,7 @@
   and     at: "at TYPE('y)"
   shows "finite (pi\<bullet>X) = finite X"
 proof -
-  have image: "(pi\<bullet>X) = (perm pi ` X)" by (force simp only: perm_set_def)
+  have image: "(pi\<bullet>X) = (perm pi ` X)" by (force simp only: perm_set_eq [OF pt at])
   show ?thesis
   proof (rule iffI)
     assume "finite (pi\<bullet>X)"
@@ -1432,17 +1438,17 @@
   and     cp:  "cp TYPE('a) TYPE('x) TYPE('y)"
   shows "(pi\<bullet>((supp x)::'y set)) = supp (pi\<bullet>x)" (is "?LHS = ?RHS")
 proof -
-  have "?LHS = {pi\<bullet>a | a. infinite {b. [(a,b)]\<bullet>x \<noteq> x}}" by (simp add: supp_def perm_set_def)
+  have "?LHS = {pi\<bullet>a | a. infinite {b. [(a,b)]\<bullet>x \<noteq> x}}" by (simp add: supp_def perm_set_eq [OF ptb at])
   also have "\<dots> = {pi\<bullet>a | a. infinite {pi\<bullet>b | b. [(a,b)]\<bullet>x \<noteq> x}}" 
   proof (rule Collect_permI, rule allI, rule iffI)
     fix a
     assume "infinite {b::'y. [(a,b)]\<bullet>x  \<noteq> x}"
     hence "infinite (pi\<bullet>{b::'y. [(a,b)]\<bullet>x \<noteq> x})" by (simp add: pt_set_infinite_ineq[OF ptb, OF at])
-    thus "infinite {pi\<bullet>b |b::'y. [(a,b)]\<bullet>x  \<noteq> x}" by (simp add: perm_set_def)
+    thus "infinite {pi\<bullet>b |b::'y. [(a,b)]\<bullet>x  \<noteq> x}" by (simp add: perm_set_eq [OF ptb at])
   next
     fix a
     assume "infinite {pi\<bullet>b |b::'y. [(a,b)]\<bullet>x \<noteq> x}"
-    hence "infinite (pi\<bullet>{b::'y. [(a,b)]\<bullet>x \<noteq> x})" by (simp add: perm_set_def)
+    hence "infinite (pi\<bullet>{b::'y. [(a,b)]\<bullet>x \<noteq> x})" by (simp add: perm_set_eq [OF ptb at])
     thus "infinite {b::'y. [(a,b)]\<bullet>x  \<noteq> x}" 
       by (simp add: pt_set_infinite_ineq[OF ptb, OF at])
   qed
@@ -1550,10 +1556,10 @@
 apply(simp add: pt_fresh_left_ineq[OF pta, OF ptb, OF at, OF cp])
 apply(drule_tac x="pi\<bullet>xa" in bspec)
 apply(simp add: pt_set_bij1[OF ptb, OF at])
-apply(simp add: set_eqvt pt_rev_pi[OF pt_list_inst[OF ptb], OF at])
+apply(simp add: set_eqvt [OF ptb at] pt_rev_pi[OF pt_list_inst[OF ptb], OF at])
 apply(simp add: pt_fresh_bij_ineq[OF pta, OF ptb, OF at, OF cp])
 apply(drule_tac x="(rev pi)\<bullet>xa" in bspec)
-apply(simp add: pt_set_bij1[OF ptb, OF at] set_eqvt)
+apply(simp add: pt_set_bij1[OF ptb, OF at] set_eqvt [OF ptb at])
 apply(simp add: pt_fresh_left_ineq[OF pta, OF ptb, OF at, OF cp])
 done
 
@@ -2012,7 +2018,8 @@
   assumes at: "at TYPE('x)"
   shows "X supports X"
 proof -
-  have "\<forall>a b. a\<notin>X \<and> b\<notin>X \<longrightarrow> [(a,b)]\<bullet>X = X" by (auto simp add: perm_set_def at_calc[OF at])
+  have "\<forall>a b. a\<notin>X \<and> b\<notin>X \<longrightarrow> [(a,b)]\<bullet>X = X"
+    by (auto simp add: perm_set_eq [OF at_pt_inst [OF at] at] at_calc[OF at])
   then show ?thesis by (simp add: supports_def)
 qed
 
@@ -2023,7 +2030,7 @@
   using a1 a2 
   apply auto
   apply (subgoal_tac "infinite (X - {b\<in>X. P b})")
-  apply (simp add: set_diff_def)
+  apply (simp add: set_diff_eq)
   apply (simp add: Diff_infinite_finite)
   done
 
@@ -2038,7 +2045,8 @@
   have inf: "infinite (UNIV-X)" using at4[OF at] fs by (auto simp add: Diff_infinite_finite)
   { fix a::"'x"
     assume asm: "a\<in>X"
-    hence "\<forall>b\<in>(UNIV-X). [(a,b)]\<bullet>X\<noteq>X" by (auto simp add: perm_set_def at_calc[OF at])
+    hence "\<forall>b\<in>(UNIV-X). [(a,b)]\<bullet>X\<noteq>X"
+      by (auto simp add: perm_set_eq [OF at_pt_inst [OF at] at] at_calc[OF at])
     with inf have "infinite {b\<in>(UNIV-X). [(a,b)]\<bullet>X\<noteq>X}" by (rule infinite_Collection)
     hence "infinite {b. [(a,b)]\<bullet>X\<noteq>X}" by (rule_tac infinite_super, auto)
     hence "a\<in>(supp X)" by (simp add: supp_def)
@@ -2259,7 +2267,7 @@
   proof (rule equalityI)
     case goal1
     show "pi\<bullet>(\<Union>x\<in>X. f x) \<subseteq> (\<Union>x\<in>(pi\<bullet>X). (pi\<bullet>f) x)"
-      apply(auto simp add: perm_set_def)
+      apply(auto simp add: perm_set_eq [OF pt at] perm_set_eq [OF at_pt_inst [OF at] at])
       apply(rule_tac x="pi\<bullet>xb" in exI)
       apply(rule conjI)
       apply(rule_tac x="xb" in exI)
@@ -2275,7 +2283,7 @@
   next
     case goal2
     show "(\<Union>x\<in>(pi\<bullet>X). (pi\<bullet>f) x) \<subseteq> pi\<bullet>(\<Union>x\<in>X. f x)"
-      apply(auto simp add: perm_set_def)
+      apply(auto simp add: perm_set_eq [OF pt at] perm_set_eq [OF at_pt_inst [OF at] at])
       apply(rule_tac x="(rev pi)\<bullet>x" in exI)
       apply(rule conjI)
       apply(simp add: pt_pi_rev[OF pt_x, OF at])
@@ -2294,7 +2302,7 @@
   and     at: "at TYPE('x)"
   shows "pi\<bullet>(X_to_Un_supp X) = ((X_to_Un_supp (pi\<bullet>X))::'x set)"
   apply(simp add: X_to_Un_supp_def)
-  apply(simp add: UNION_f_eqvt[OF pt, OF at] perm_fun_def)
+  apply(simp add: UNION_f_eqvt[OF pt, OF at] perm_fun_def [where 'b="'x set"])
   apply(simp add: pt_perm_supp[OF pt, OF at])
   apply(simp add: pt_pi_rev[OF pt, OF at])
   done
@@ -2308,7 +2316,7 @@
   apply(rule allI)+
   apply(rule impI)
   apply(erule conjE)
-  apply(simp add: perm_set_def)
+  apply(simp add: perm_set_eq [OF pt at])
   apply(auto)
   apply(subgoal_tac "[(a,b)]\<bullet>xa = xa")(*A*)
   apply(simp)
@@ -2339,9 +2347,9 @@
 proof -
   have "supp ((X_to_Un_supp X)::'x set) \<subseteq> ((supp X)::'x set)"  
     apply(rule pt_empty_supp_fun_subset)
-    apply(force intro: pt_set_inst at_pt_inst pt at)+
+    apply(force intro: pt_fun_inst pt_bool_inst at_pt_inst pt at)+
     apply(rule pt_eqvt_fun2b)
-    apply(force intro: pt_set_inst at_pt_inst pt at)+
+    apply(force intro: pt_fun_inst pt_bool_inst at_pt_inst pt at)+
     apply(rule allI)+
     apply(rule X_to_Un_supp_eqvt[OF pt, OF at])
     done
@@ -2392,7 +2400,7 @@
   also have "\<dots> = (supp {x})\<union>(supp X)"
     by (rule supp_fin_union[OF pt, OF at, OF fs], simp_all add: f)
   finally show "(supp (insert x X)) = (supp x)\<union>((supp X)::'x set)" 
-    by (simp add: supp_singleton)
+    by (simp add: supp_singleton [OF pt at])
 qed
 
 lemma fresh_fin_union:
@@ -2477,17 +2485,6 @@
 apply(auto)
 done
 
-lemma cp_set_inst:
-  assumes c1: "cp TYPE ('a) TYPE('x) TYPE('y)"
-  shows "cp TYPE ('a set) TYPE('x) TYPE('y)"
-using c1
-apply(simp add: cp_def)
-apply(auto)
-apply(auto simp add: perm_set_def)
-apply(rule_tac x="pi2\<bullet>xc" in exI)
-apply(auto)
-done
-
 lemma cp_option_inst:
   assumes c1: "cp TYPE ('a) TYPE('x) TYPE('y)"
   shows "cp TYPE ('a option) TYPE('x) TYPE('y)"
@@ -3369,7 +3366,7 @@
   plus_int_eqvt minus_int_eqvt mult_int_eqvt div_int_eqvt
   
   (* sets *)
-  union_eqvt empty_eqvt insert_eqvt set_eqvt 
+  union_eqvt empty_eqvt
   
  
 (* the lemmas numeral_nat_eqvt numeral_int_eqvt do not conform with the *)
diff -r 27941d7d9a11 -r 40b411ec05aa src/HOL/Nominal/nominal_package.ML
--- a/src/HOL/Nominal/nominal_package.ML	Wed May 07 10:56:58 2008 +0200
+++ b/src/HOL/Nominal/nominal_package.ML	Wed May 07 10:57:19 2008 +0200
@@ -1183,8 +1183,9 @@
 
     val ind_prems' =
       map (fn (_, f as Free (_, T)) => list_all_free ([("x", fsT')],
-        HOLogic.mk_Trueprop (Const ("Finite_Set.finite", body_type T -->
-          HOLogic.boolT) $ (f $ Free ("x", fsT'))))) fresh_fs @
+        HOLogic.mk_Trueprop (Const ("Finite_Set.finite",
+          (snd (split_last (binder_types T)) --> HOLogic.boolT) -->
+            HOLogic.boolT) $ (f $ Free ("x", fsT'))))) fresh_fs @
       List.concat (map (fn (((i, (_, _, constrs)), (_, idxss)), T) =>
         map (make_ind_prem fsT' (fn T => fn t => fn u => HOLogic.Not $
           HOLogic.mk_mem (t, the (AList.lookup op = fresh_fs T) $ u)) i T)
diff -r 27941d7d9a11 -r 40b411ec05aa src/HOL/Nominal/nominal_permeq.ML
--- a/src/HOL/Nominal/nominal_permeq.ML	Wed May 07 10:56:58 2008 +0200
+++ b/src/HOL/Nominal/nominal_permeq.ML	Wed May 07 10:57:19 2008 +0200
@@ -290,7 +290,7 @@
 fun finite_guess_tac tactical ss i st =
     let val goal = List.nth(cprems_of st, i-1)
     in
-      case Logic.strip_assums_concl (term_of goal) of
+      case Envir.eta_contract (Logic.strip_assums_concl (term_of goal)) of
           _ $ (Const ("Finite_Set.finite", _) $ (Const ("Nominal.supp", T) $ x)) =>
           let
             val cert = Thm.cterm_of (Thm.theory_of_thm st);
@@ -301,7 +301,8 @@
                 HOLogic.pair_const (fastype_of1 (Ts, v)) (fastype_of1 (Ts, s)) $ v $ s)
               (vs, HOLogic.unit);
             val s' = list_abs (ps,
-              Const ("Nominal.supp", fastype_of1 (Ts, s) --> body_type T) $ s);
+              Const ("Nominal.supp", fastype_of1 (Ts, s) -->
+                snd (split_last (binder_types T)) --> HOLogic.boolT) $ s);
             val supports_rule' = Thm.lift_rule goal supports_rule;
             val _ $ (_ $ S $ _) =
               Logic.strip_assums_concl (hd (prems_of supports_rule'));
diff -r 27941d7d9a11 -r 40b411ec05aa src/HOL/Real/PReal.thy
--- a/src/HOL/Real/PReal.thy	Wed May 07 10:56:58 2008 +0200
+++ b/src/HOL/Real/PReal.thy	Wed May 07 10:57:19 2008 +0200
@@ -202,7 +202,7 @@
 
 (* Axiom 'order_less_le' of class 'order': *)
 lemma preal_less_le: "((w::preal) < z) = (w \<le> z & w \<noteq> z)"
-by (simp add: preal_le_def preal_less_def Rep_preal_inject psubset_def)
+by (simp add: preal_le_def preal_less_def Rep_preal_inject less_le)
 
 instance preal :: order
   by intro_classes
@@ -943,7 +943,7 @@
 
 text{*at last, Gleason prop. 9-3.5(iii) page 123*}
 lemma preal_self_less_add_left: "(R::preal) < R + S"
-apply (unfold preal_less_def psubset_def)
+apply (unfold preal_less_def less_le)
 apply (simp add: Rep_preal_self_subset Rep_preal_sum_not_eq [THEN not_sym])
 done
 
diff -r 27941d7d9a11 -r 40b411ec05aa src/HOL/Subst/Unify.thy
--- a/src/HOL/Subst/Unify.thy	Wed May 07 10:56:58 2008 +0200
+++ b/src/HOL/Subst/Unify.thy	Wed May 07 10:57:19 2008 +0200
@@ -117,7 +117,7 @@
 apply blast
 txt{*@{text finite_psubset} case*}
 apply (simp add: unifyRel_def lex_prod_def)
-apply (simp add: finite_psubset_def finite_vars_of psubset_def)
+apply (simp add: finite_psubset_def finite_vars_of psubset_eq)
 apply blast
 txt{*Final case, also @{text finite_psubset}*}
 apply (simp add: finite_vars_of unifyRel_def finite_psubset_def lex_prod_def)
diff -r 27941d7d9a11 -r 40b411ec05aa src/HOL/Tools/datatype_rep_proofs.ML
--- a/src/HOL/Tools/datatype_rep_proofs.ML	Wed May 07 10:56:58 2008 +0200
+++ b/src/HOL/Tools/datatype_rep_proofs.ML	Wed May 07 10:57:19 2008 +0200
@@ -375,12 +375,16 @@
                (map (pair "x") Ts, S $ app_bnds f i)),
              HOLogic.mk_Trueprop (HOLogic.mk_eq (list_abs (map (pair "x") Ts,
                r $ (a $ app_bnds f i)), f))))
-            (fn _ => EVERY [REPEAT (rtac ext 1), REPEAT (etac allE 1), rtac thm 1, atac 1])
+            (fn _ => EVERY [REPEAT_DETERM_N i (rtac ext 1),
+               REPEAT (etac allE 1), rtac thm 1, atac 1])
           end
       in map (fn r => r RS subst) (thm :: map mk_thm arities) end;
 
     (* prove  inj dt_Rep_i  and  dt_Rep_i x : dt_rep_set_i *)
 
+    val fun_congs = map (fn T => make_elim (Drule.instantiate'
+      [SOME (ctyp_of thy5 T)] [] fun_cong)) branchTs;
+
     fun prove_iso_thms (ds, (inj_thms, elem_thms)) =
       let
         val (_, (tname, _, _)) = hd ds;
@@ -422,7 +426,7 @@
                         [REPEAT (rtac ext 1),
                          REPEAT (eresolve_tac (mp :: allE ::
                            map make_elim (Suml_inject :: Sumr_inject ::
-                             Lim_inject :: fun_cong :: inj_thms')) 1),
+                             Lim_inject :: inj_thms') @ fun_congs) 1),
                          atac 1]))])])])]);
 
         val inj_thms'' = map (fn r => r RS @{thm datatype_injI})
diff -r 27941d7d9a11 -r 40b411ec05aa src/HOL/Tools/inductive_codegen.ML
--- a/src/HOL/Tools/inductive_codegen.ML	Wed May 07 10:56:58 2008 +0200
+++ b/src/HOL/Tools/inductive_codegen.ML	Wed May 07 10:57:19 2008 +0200
@@ -191,11 +191,11 @@
     | _ => default)
   end;
 
-datatype indprem = Prem of term list * term | Sidecond of term;
+datatype indprem = Prem of term list * term * bool | Sidecond of term;
 
 fun select_mode_prem thy modes vs ps =
   find_first (is_some o snd) (ps ~~ map
-    (fn Prem (us, t) => find_first (fn Mode (_, is, _) =>
+    (fn Prem (us, t, is_set) => find_first (fn Mode (_, is, _) =>
           let
             val (in_ts, out_ts) = get_args is 1 us;
             val (out_ts', in_ts') = List.partition (is_constrt thy) out_ts;
@@ -208,7 +208,9 @@
             term_vs t subset vs andalso
             forall is_eqT dupTs
           end)
-            (modes_of modes t handle Option => [Mode (([], []), [], [])])
+            (if is_set then [Mode (([], []), [], [])]
+             else modes_of modes t handle Option =>
+               error ("Bad predicate: " ^ Sign.string_of_term thy t))
       | Sidecond t => if term_vs t subset vs then SOME (Mode (([], []), [], []))
           else NONE) ps);
 
@@ -221,7 +223,7 @@
       | check_mode_prems vs ps = (case select_mode_prem thy modes' vs ps of
           NONE => NONE
         | SOME (x, _) => check_mode_prems
-            (case x of Prem (us, _) => vs union terms_vs us | _ => vs)
+            (case x of Prem (us, _, _) => vs union terms_vs us | _ => vs)
             (filter_out (equal x) ps));
     val (in_ts, in_ts') = List.partition (is_constrt thy) (fst (get_args is 1 ts));
     val in_vs = terms_vs in_ts;
@@ -390,21 +392,21 @@
             val (gr1, eq_ps) = foldl_map compile_eq (gr0, eqs)
           in
             (case p of
-               Prem (us, t) =>
+               Prem (us, t, is_set) =>
                  let
                    val (in_ts, out_ts''') = get_args js 1 us;
                    val (gr2, in_ps) = foldl_map
                      (invoke_codegen thy defs dep module true) (gr1, in_ts);
-                   val (gr3, ps) = (case body_type (fastype_of t) of
-                       Type ("bool", []) =>
+                   val (gr3, ps) =
+                     if not is_set then
                        apsnd (fn ps => ps @
                            (if null in_ps then [] else [Pretty.brk 1]) @
                            separate (Pretty.brk 1) in_ps)
                          (compile_expr thy defs dep module false modes
                            (gr2, (mode, t)))
-                     | _ =>
+                     else
                        apsnd (fn p => [Pretty.str "DSeq.of_list", Pretty.brk 1, p])
-                           (invoke_codegen thy defs dep module true (gr2, t)));
+                           (invoke_codegen thy defs dep module true (gr2, t));
                    val (gr4, rest) = compile_prems out_ts''' vs' (fst nvs) gr3 ps';
                  in
                    (gr4, compile_match (snd nvs) eq_ps out_ps
@@ -504,16 +506,16 @@
       fun get_nparms s = if s mem names then SOME nparms else
         Option.map #3 (get_clauses thy s);
 
-      fun dest_prem (_ $ (Const ("op :", _) $ t $ u)) = Prem ([t], u)
-        | dest_prem (_ $ ((eq as Const ("op =", _)) $ t $ u)) = Prem ([t, u], eq)
+      fun dest_prem (_ $ (Const ("op :", _) $ t $ u)) = Prem ([t], Envir.beta_eta_contract u, true)
+        | dest_prem (_ $ ((eq as Const ("op =", _)) $ t $ u)) = Prem ([t, u], eq, false)
         | dest_prem (_ $ t) =
             (case strip_comb t of
-               (v as Var _, ts) => if v mem args then Prem (ts, v) else Sidecond t
+               (v as Var _, ts) => if v mem args then Prem (ts, v, false) else Sidecond t
              | (c as Const (s, _), ts) => (case get_nparms s of
                  NONE => Sidecond t
                | SOME k =>
                    let val (ts1, ts2) = chop k ts
-                   in Prem (ts2, list_comb (c, ts1)) end)
+                   in Prem (ts2, list_comb (c, ts1), false) end)
              | _ => Sidecond t);
 
       fun add_clause intr (clauses, arities) =
diff -r 27941d7d9a11 -r 40b411ec05aa src/HOL/Tools/inductive_set_package.ML
--- a/src/HOL/Tools/inductive_set_package.ML	Wed May 07 10:56:58 2008 +0200
+++ b/src/HOL/Tools/inductive_set_package.ML	Wed May 07 10:57:19 2008 +0200
@@ -237,7 +237,7 @@
         NONE => thm' RS sym
       | SOME fs' =>
           let
-            val U = HOLogic.dest_setT (body_type T);
+            val (_, U) = split_last (binder_types T);
             val Ts = HOLogic.prodT_factors' fs' U;
             (* FIXME: should cterm_instantiate increment indexes? *)
             val arg_cong' = Thm.incr_indexes (Thm.maxidx_of thm + 1) arg_cong;
@@ -413,7 +413,7 @@
       | infer (t $ u) = infer t #> infer u
       | infer _ = I;
     val new_arities = filter_out
-      (fn (x as Free (_, Type ("fun", _)), _) => x mem params
+      (fn (x as Free (_, T), _) => x mem params andalso length (binder_types T) > 1
         | _ => false) (fold (snd #> infer) intros []);
     val params' = map (fn x => (case AList.lookup op = new_arities x of
         SOME fs =>
@@ -437,7 +437,7 @@
     val ((cs', cs_info), eqns) = cs |> map (fn c as Free (s, T) =>
       let
         val fs = the_default [] (AList.lookup op = new_arities c);
-        val U = HOLogic.dest_setT (body_type T);
+        val (_, U) = split_last (binder_types T);
         val Ts = HOLogic.prodT_factors' fs U;
         val c' = Free (s ^ "p",
           map fastype_of params1 @ Ts ---> HOLogic.boolT)
diff -r 27941d7d9a11 -r 40b411ec05aa src/HOL/UNITY/ELT.thy
--- a/src/HOL/UNITY/ELT.thy	Wed May 07 10:56:58 2008 +0200
+++ b/src/HOL/UNITY/ELT.thy	Wed May 07 10:57:19 2008 +0200
@@ -102,7 +102,7 @@
 apply (simp (no_asm_use) add: givenBy_eq_Collect)
 apply safe
 apply (rule_tac x = "%z. ?R z & ~ ?Q z" in exI)
-unfolding set_diff_def
+unfolding set_diff_eq
 apply auto
 done
 
diff -r 27941d7d9a11 -r 40b411ec05aa src/HOL/UNITY/Transformers.thy
--- a/src/HOL/UNITY/Transformers.thy	Wed May 07 10:56:58 2008 +0200
+++ b/src/HOL/UNITY/Transformers.thy	Wed May 07 10:57:19 2008 +0200
@@ -88,7 +88,7 @@
 done
 
 lemma wens_Id [simp]: "wens F Id B = B"
-by (simp add: wens_def gfp_def wp_def awp_def Sup_set_def, blast)
+by (simp add: wens_def gfp_def wp_def awp_def Sup_set_eq, blast)
 
 text{*These two theorems justify the claim that @{term wens} returns the
 weakest assertion satisfying the ensures property*}
@@ -101,7 +101,7 @@
 
 lemma wens_ensures: "act \<in> Acts F ==> F \<in> (wens F act B) ensures B"
 by (simp add: wens_def gfp_def constrains_def awp_def wp_def
-              ensures_def transient_def Sup_set_def, blast)
+              ensures_def transient_def Sup_set_eq, blast)
 
 text{*These two results constitute assertion (4.13) of the thesis*}
 lemma wens_mono: "(A \<subseteq> B) ==> wens F act A \<subseteq> wens F act B"
@@ -110,7 +110,7 @@
 done
 
 lemma wens_weakening: "B \<subseteq> wens F act B"
-by (simp add: wens_def gfp_def Sup_set_def, blast)
+by (simp add: wens_def gfp_def Sup_set_eq, blast)
 
 text{*Assertion (6), or 4.16 in the thesis*}
 lemma subset_wens: "A-B \<subseteq> wp act B \<inter> awp F (B \<union> A) ==> A \<subseteq> wens F act B" 
@@ -120,7 +120,7 @@
 
 text{*Assertion 4.17 in the thesis*}
 lemma Diff_wens_constrains: "F \<in> (wens F act A - A) co wens F act A"
-by (simp add: wens_def gfp_def wp_def awp_def constrains_def Sup_set_def, blast)
+by (simp add: wens_def gfp_def wp_def awp_def constrains_def Sup_set_eq, blast)
   --{*Proved instantly, yet remarkably fragile. If @{text Un_subset_iff}
       is declared as an iff-rule, then it's almost impossible to prove. 
       One proof is via @{text meson} after expanding all definitions, but it's
@@ -331,7 +331,7 @@
 
 lemma wens_single_eq:
      "wens (mk_program (init, {act}, allowed)) act B = B \<union> wp act B"
-by (simp add: wens_def gfp_def wp_def Sup_set_def, blast)
+by (simp add: wens_def gfp_def wp_def Sup_set_eq, blast)
 
 
 text{*Next, we express the @{term "wens_set"} for single-assignment programs*}
diff -r 27941d7d9a11 -r 40b411ec05aa src/HOLCF/CompactBasis.thy
--- a/src/HOLCF/CompactBasis.thy	Wed May 07 10:56:58 2008 +0200
+++ b/src/HOLCF/CompactBasis.thy	Wed May 07 10:57:19 2008 +0200
@@ -227,7 +227,7 @@
 
 lemma lessI: "(\<And>a. principal a \<sqsubseteq> x \<Longrightarrow> principal a \<sqsubseteq> u) \<Longrightarrow> x \<sqsubseteq> u"
 unfolding principal_less_iff
-by (simp add: less_def subset_def)
+by (simp add: less_def subset_eq)
 
 lemma lub_principal_approxes: "principal ` approxes x <<| x"
 apply (rule is_lubI)
diff -r 27941d7d9a11 -r 40b411ec05aa src/HOLCF/ConvexPD.thy
--- a/src/HOLCF/ConvexPD.thy	Wed May 07 10:56:58 2008 +0200
+++ b/src/HOLCF/ConvexPD.thy	Wed May 07 10:57:19 2008 +0200
@@ -151,7 +151,7 @@
 by (rule Rep_convex_pd [simplified])
 
 lemma Rep_convex_pd_mono: "xs \<sqsubseteq> ys \<Longrightarrow> Rep_convex_pd xs \<subseteq> Rep_convex_pd ys"
-unfolding less_convex_pd_def less_set_def .
+unfolding less_convex_pd_def less_set_eq .
 
 
 subsection {* Principal ideals *}
@@ -179,12 +179,12 @@
 apply (rule ideal_Rep_convex_pd)
 apply (rule cont_Rep_convex_pd)
 apply (rule Rep_convex_principal)
-apply (simp only: less_convex_pd_def less_set_def)
+apply (simp only: less_convex_pd_def less_set_eq)
 done
 
 lemma convex_principal_less_iff [simp]:
   "(convex_principal t \<sqsubseteq> convex_principal u) = (t \<le>\<natural> u)"
-unfolding less_convex_pd_def Rep_convex_principal less_set_def
+unfolding less_convex_pd_def Rep_convex_principal less_set_eq
 by (fast intro: convex_le_refl elim: convex_le_trans)
 
 lemma convex_principal_mono:
diff -r 27941d7d9a11 -r 40b411ec05aa src/HOLCF/IOA/meta_theory/Automata.thy
--- a/src/HOLCF/IOA/meta_theory/Automata.thy	Wed May 07 10:56:58 2008 +0200
+++ b/src/HOLCF/IOA/meta_theory/Automata.thy	Wed May 07 10:57:19 2008 +0200
@@ -300,33 +300,33 @@
 lemma externals_of_par: "ext (A1||A2) =     
    (ext A1) Un (ext A2)"
 apply (simp add: externals_def asig_of_par asig_comp_def
-  asig_inputs_def asig_outputs_def Un_def set_diff_def)
+  asig_inputs_def asig_outputs_def Un_def set_diff_eq)
 apply blast
 done
 
 lemma actions_of_par: "act (A1||A2) =     
    (act A1) Un (act A2)"
 apply (simp add: actions_def asig_of_par asig_comp_def
-  asig_inputs_def asig_outputs_def asig_internals_def Un_def set_diff_def)
+  asig_inputs_def asig_outputs_def asig_internals_def Un_def set_diff_eq)
 apply blast
 done
 
 lemma inputs_of_par: "inp (A1||A2) = 
           ((inp A1) Un (inp A2)) - ((out A1) Un (out A2))"
 apply (simp add: actions_def asig_of_par asig_comp_def
-  asig_inputs_def asig_outputs_def Un_def set_diff_def)
+  asig_inputs_def asig_outputs_def Un_def set_diff_eq)
 done
 
 lemma outputs_of_par: "out (A1||A2) = 
           (out A1) Un (out A2)"
 apply (simp add: actions_def asig_of_par asig_comp_def
-  asig_outputs_def Un_def set_diff_def)
+  asig_outputs_def Un_def set_diff_eq)
 done
 
 lemma internals_of_par: "int (A1||A2) = 
           (int A1) Un (int A2)"
 apply (simp add: actions_def asig_of_par asig_comp_def
-  asig_inputs_def asig_outputs_def asig_internals_def Un_def set_diff_def)
+  asig_inputs_def asig_outputs_def asig_internals_def Un_def set_diff_eq)
 done
 
 
diff -r 27941d7d9a11 -r 40b411ec05aa src/HOLCF/LowerPD.thy
--- a/src/HOLCF/LowerPD.thy	Wed May 07 10:56:58 2008 +0200
+++ b/src/HOLCF/LowerPD.thy	Wed May 07 10:57:19 2008 +0200
@@ -106,7 +106,7 @@
 by (rule Rep_lower_pd [simplified])
 
 lemma Rep_lower_pd_mono: "x \<sqsubseteq> y \<Longrightarrow> Rep_lower_pd x \<subseteq> Rep_lower_pd y"
-unfolding less_lower_pd_def less_set_def .
+unfolding less_lower_pd_def less_set_eq .
 
 
 subsection {* Principal ideals *}
@@ -134,12 +134,12 @@
 apply (rule ideal_Rep_lower_pd)
 apply (rule cont_Rep_lower_pd)
 apply (rule Rep_lower_principal)
-apply (simp only: less_lower_pd_def less_set_def)
+apply (simp only: less_lower_pd_def less_set_eq)
 done
 
 lemma lower_principal_less_iff [simp]:
   "(lower_principal t \<sqsubseteq> lower_principal u) = (t \<le>\<flat> u)"
-unfolding less_lower_pd_def Rep_lower_principal less_set_def
+unfolding less_lower_pd_def Rep_lower_principal less_set_eq
 by (fast intro: lower_le_refl elim: lower_le_trans)
 
 lemma lower_principal_mono:
@@ -151,7 +151,7 @@
 apply (simp add: less_lower_pd_def)
 apply (simp add: cont2contlubE [OF cont_Rep_lower_pd])
 apply (simp add: Rep_lower_principal set_cpo_simps)
-apply (simp add: subset_def)
+apply (simp add: subset_eq)
 apply (drule spec, drule mp, rule lower_le_refl)
 apply (erule exE, rename_tac i)
 apply (rule_tac x=i in exI)
diff -r 27941d7d9a11 -r 40b411ec05aa src/HOLCF/UpperPD.thy
--- a/src/HOLCF/UpperPD.thy	Wed May 07 10:56:58 2008 +0200
+++ b/src/HOLCF/UpperPD.thy	Wed May 07 10:57:19 2008 +0200
@@ -126,12 +126,12 @@
 apply (rule ideal_Rep_upper_pd)
 apply (rule cont_Rep_upper_pd)
 apply (rule Rep_upper_principal)
-apply (simp only: less_upper_pd_def less_set_def)
+apply (simp only: less_upper_pd_def less_set_eq)
 done
 
 lemma upper_principal_less_iff [simp]:
   "(upper_principal t \<sqsubseteq> upper_principal u) = (t \<le>\<sharp> u)"
-unfolding less_upper_pd_def Rep_upper_principal less_set_def
+unfolding less_upper_pd_def Rep_upper_principal less_set_eq
 by (fast intro: upper_le_refl elim: upper_le_trans)
 
 lemma upper_principal_mono: