# HG changeset patch
# User haftmann
# Date 1315243118 -7200
# Node ID 27fb2285bdeeb3214158a0fb9e83b1cbbb8c1d2e
# Parent  487ae6317f7bca261a4e0c5bbb0e04344d665c4b# Parent  4ea8489593402176f8c64476fb32880c0e855cc5
merged

diff -r 487ae6317f7b -r 27fb2285bdee src/HOL/Finite_Set.thy
--- a/src/HOL/Finite_Set.thy	Sun Sep 04 06:27:59 2011 -0700
+++ b/src/HOL/Finite_Set.thy	Mon Sep 05 19:18:38 2011 +0200
@@ -486,22 +486,9 @@
 
 end
 
-instance unit :: finite proof
-qed (simp add: UNIV_unit)
-
-instance bool :: finite proof
-qed (simp add: UNIV_bool)
-
 instance prod :: (finite, finite) finite proof
 qed (simp only: UNIV_Times_UNIV [symmetric] finite_cartesian_product finite)
 
-lemma finite_option_UNIV [simp]:
-  "finite (UNIV :: 'a option set) = finite (UNIV :: 'a set)"
-  by (auto simp add: UNIV_option_conv elim: finite_imageD intro: inj_Some)
-
-instance option :: (finite) finite proof
-qed (simp add: UNIV_option_conv)
-
 lemma inj_graph: "inj (%f. {(x, y). y = f x})"
   by (rule inj_onI, auto simp add: set_eq_iff fun_eq_iff)
 
@@ -519,9 +506,22 @@
   qed
 qed
 
+instance bool :: finite proof
+qed (simp add: UNIV_bool)
+
+instance unit :: finite proof
+qed (simp add: UNIV_unit)
+
 instance sum :: (finite, finite) finite proof
 qed (simp only: UNIV_Plus_UNIV [symmetric] finite_Plus finite)
 
+lemma finite_option_UNIV [simp]:
+  "finite (UNIV :: 'a option set) = finite (UNIV :: 'a set)"
+  by (auto simp add: UNIV_option_conv elim: finite_imageD intro: inj_Some)
+
+instance option :: (finite) finite proof
+qed (simp add: UNIV_option_conv)
+
 
 subsection {* A basic fold functional for finite sets *}
 
diff -r 487ae6317f7b -r 27fb2285bdee src/HOL/Nominal/nominal_permeq.ML
--- a/src/HOL/Nominal/nominal_permeq.ML	Sun Sep 04 06:27:59 2011 -0700
+++ b/src/HOL/Nominal/nominal_permeq.ML	Mon Sep 05 19:18:38 2011 +0200
@@ -130,7 +130,7 @@
      case redex of 
        (* case pi o f == (%x. pi o (f ((rev pi)o x))) *)     
        (Const("Nominal.perm",_) $ pi $ f)  => 
-          (if (applicable_fun f) then SOME perm_fun_def else NONE)
+          (if applicable_fun f then SOME perm_fun_def else NONE)
       | _ => NONE
    end