assert Pure equations for theorem references; tuned

--- a/src/HOL/Nominal/nominal_atoms.ML	Sat Sep 03 17:32:34 2011 +0200
+++ b/src/HOL/Nominal/nominal_atoms.ML	Sat Sep 03 17:32:34 2011 +0200
@@ -714,48 +714,48 @@
              fold (fn ak_name => fn thy =>
              let
                val qu_class = Sign.full_bname thy ("pt_"^ak_name);
-               val simp_s = HOL_basic_ss addsimps [defn];
+               val simp_s = HOL_basic_ss addsimps [Simpdata.mk_eq defn];
                val proof = EVERY [Class.intro_classes_tac [], REPEAT (asm_simp_tac simp_s 1)];
              in 
-               AxClass.prove_arity (discrete_ty,[],[qu_class]) proof thy
+               AxClass.prove_arity (discrete_ty, [], [qu_class]) proof thy
              end) ak_names;
 
           fun discrete_fs_inst discrete_ty defn = 
              fold (fn ak_name => fn thy =>
              let
                val qu_class = Sign.full_bname thy ("fs_"^ak_name);
-               val supp_def = @{thm "Nominal.supp_def"};
-               val simp_s = HOL_ss addsimps [supp_def,Collect_const,finite_emptyI,defn];
+               val supp_def = Simpdata.mk_eq @{thm "Nominal.supp_def"};
+               val simp_s = HOL_ss addsimps [supp_def, Collect_const, finite_emptyI, Simpdata.mk_eq defn];
                val proof = EVERY [Class.intro_classes_tac [], asm_simp_tac simp_s 1];
              in 
-               AxClass.prove_arity (discrete_ty,[],[qu_class]) proof thy
+               AxClass.prove_arity (discrete_ty, [], [qu_class]) proof thy
              end) ak_names;
 
           fun discrete_cp_inst discrete_ty defn = 
              fold (fn ak_name' => (fold (fn ak_name => fn thy =>
              let
                val qu_class = Sign.full_bname thy ("cp_"^ak_name^"_"^ak_name');
-               val supp_def = @{thm "Nominal.supp_def"};
-               val simp_s = HOL_ss addsimps [defn];
+               val supp_def = Simpdata.mk_eq @{thm "Nominal.supp_def"};
+               val simp_s = HOL_ss addsimps [Simpdata.mk_eq defn];
                val proof = EVERY [Class.intro_classes_tac [], asm_simp_tac simp_s 1];
              in
-               AxClass.prove_arity (discrete_ty,[],[qu_class]) proof thy
+               AxClass.prove_arity (discrete_ty, [], [qu_class]) proof thy
              end) ak_names)) ak_names;
 
         in
          thy26
-         |> discrete_pt_inst @{type_name nat}  @{thm "perm_nat_def"}
-         |> discrete_fs_inst @{type_name nat}  @{thm "perm_nat_def"}
-         |> discrete_cp_inst @{type_name nat}  @{thm "perm_nat_def"}
-         |> discrete_pt_inst @{type_name bool} @{thm "perm_bool"}
-         |> discrete_fs_inst @{type_name bool} @{thm "perm_bool"}
-         |> discrete_cp_inst @{type_name bool} @{thm "perm_bool"}
-         |> discrete_pt_inst @{type_name int} @{thm "perm_int_def"}
-         |> discrete_fs_inst @{type_name int} @{thm "perm_int_def"}
-         |> discrete_cp_inst @{type_name int} @{thm "perm_int_def"}
-         |> discrete_pt_inst @{type_name char} @{thm "perm_char_def"}
-         |> discrete_fs_inst @{type_name char} @{thm "perm_char_def"}
-         |> discrete_cp_inst @{type_name char} @{thm "perm_char_def"}
+         |> discrete_pt_inst @{type_name nat} @{thm perm_nat_def}
+         |> discrete_fs_inst @{type_name nat} @{thm perm_nat_def}
+         |> discrete_cp_inst @{type_name nat} @{thm perm_nat_def}
+         |> discrete_pt_inst @{type_name bool} @{thm perm_bool}
+         |> discrete_fs_inst @{type_name bool} @{thm perm_bool}
+         |> discrete_cp_inst @{type_name bool} @{thm perm_bool}
+         |> discrete_pt_inst @{type_name int} @{thm perm_int_def}
+         |> discrete_fs_inst @{type_name int} @{thm perm_int_def}
+         |> discrete_cp_inst @{type_name int} @{thm perm_int_def}
+         |> discrete_pt_inst @{type_name char} @{thm perm_char_def}
+         |> discrete_fs_inst @{type_name char} @{thm perm_char_def}
+         |> discrete_cp_inst @{type_name char} @{thm perm_char_def}
         end;
 
 

--- a/src/HOL/Nominal/nominal_permeq.ML	Sat Sep 03 17:32:34 2011 +0200
+++ b/src/HOL/Nominal/nominal_permeq.ML	Sat Sep 03 17:32:34 2011 +0200
@@ -56,10 +56,10 @@
 val finite_Un     = @{thm "finite_Un"};
 val conj_absorb   = @{thm "conj_absorb"};
 val not_false     = @{thm "not_False_eq_True"}
-val perm_fun_def  = @{thm "Nominal.perm_fun_def"};
+val perm_fun_def  = Simpdata.mk_eq @{thm "Nominal.perm_fun_def"};
 val perm_eq_app   = @{thm "Nominal.pt_fun_app_eq"};
-val supports_def  = @{thm "Nominal.supports_def"};
-val fresh_def     = @{thm "Nominal.fresh_def"};
+val supports_def  = Simpdata.mk_eq @{thm "Nominal.supports_def"};
+val fresh_def     = Simpdata.mk_eq @{thm "Nominal.fresh_def"};
 val fresh_prod    = @{thm "Nominal.fresh_prod"};
 val fresh_unit    = @{thm "Nominal.fresh_unit"};
 val supports_rule = @{thm "supports_finite"};
@@ -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