src/HOL/Nominal/nominal_atoms.ML
changeset 44684 8dde3352d5c4
parent 41562 90fb3d7474df
child 44689 f247fc952f31
     1.1 --- a/src/HOL/Nominal/nominal_atoms.ML	Sat Sep 03 17:32:34 2011 +0200
     1.2 +++ b/src/HOL/Nominal/nominal_atoms.ML	Sat Sep 03 17:32:34 2011 +0200
     1.3 @@ -714,48 +714,48 @@
     1.4               fold (fn ak_name => fn thy =>
     1.5               let
     1.6                 val qu_class = Sign.full_bname thy ("pt_"^ak_name);
     1.7 -               val simp_s = HOL_basic_ss addsimps [defn];
     1.8 +               val simp_s = HOL_basic_ss addsimps [Simpdata.mk_eq defn];
     1.9                 val proof = EVERY [Class.intro_classes_tac [], REPEAT (asm_simp_tac simp_s 1)];
    1.10               in 
    1.11 -               AxClass.prove_arity (discrete_ty,[],[qu_class]) proof thy
    1.12 +               AxClass.prove_arity (discrete_ty, [], [qu_class]) proof thy
    1.13               end) ak_names;
    1.14  
    1.15            fun discrete_fs_inst discrete_ty defn = 
    1.16               fold (fn ak_name => fn thy =>
    1.17               let
    1.18                 val qu_class = Sign.full_bname thy ("fs_"^ak_name);
    1.19 -               val supp_def = @{thm "Nominal.supp_def"};
    1.20 -               val simp_s = HOL_ss addsimps [supp_def,Collect_const,finite_emptyI,defn];
    1.21 +               val supp_def = Simpdata.mk_eq @{thm "Nominal.supp_def"};
    1.22 +               val simp_s = HOL_ss addsimps [supp_def, Collect_const, finite_emptyI, Simpdata.mk_eq defn];
    1.23                 val proof = EVERY [Class.intro_classes_tac [], asm_simp_tac simp_s 1];
    1.24               in 
    1.25 -               AxClass.prove_arity (discrete_ty,[],[qu_class]) proof thy
    1.26 +               AxClass.prove_arity (discrete_ty, [], [qu_class]) proof thy
    1.27               end) ak_names;
    1.28  
    1.29            fun discrete_cp_inst discrete_ty defn = 
    1.30               fold (fn ak_name' => (fold (fn ak_name => fn thy =>
    1.31               let
    1.32                 val qu_class = Sign.full_bname thy ("cp_"^ak_name^"_"^ak_name');
    1.33 -               val supp_def = @{thm "Nominal.supp_def"};
    1.34 -               val simp_s = HOL_ss addsimps [defn];
    1.35 +               val supp_def = Simpdata.mk_eq @{thm "Nominal.supp_def"};
    1.36 +               val simp_s = HOL_ss addsimps [Simpdata.mk_eq defn];
    1.37                 val proof = EVERY [Class.intro_classes_tac [], asm_simp_tac simp_s 1];
    1.38               in
    1.39 -               AxClass.prove_arity (discrete_ty,[],[qu_class]) proof thy
    1.40 +               AxClass.prove_arity (discrete_ty, [], [qu_class]) proof thy
    1.41               end) ak_names)) ak_names;
    1.42  
    1.43          in
    1.44           thy26
    1.45 -         |> discrete_pt_inst @{type_name nat}  @{thm "perm_nat_def"}
    1.46 -         |> discrete_fs_inst @{type_name nat}  @{thm "perm_nat_def"}
    1.47 -         |> discrete_cp_inst @{type_name nat}  @{thm "perm_nat_def"}
    1.48 -         |> discrete_pt_inst @{type_name bool} @{thm "perm_bool"}
    1.49 -         |> discrete_fs_inst @{type_name bool} @{thm "perm_bool"}
    1.50 -         |> discrete_cp_inst @{type_name bool} @{thm "perm_bool"}
    1.51 -         |> discrete_pt_inst @{type_name int} @{thm "perm_int_def"}
    1.52 -         |> discrete_fs_inst @{type_name int} @{thm "perm_int_def"}
    1.53 -         |> discrete_cp_inst @{type_name int} @{thm "perm_int_def"}
    1.54 -         |> discrete_pt_inst @{type_name char} @{thm "perm_char_def"}
    1.55 -         |> discrete_fs_inst @{type_name char} @{thm "perm_char_def"}
    1.56 -         |> discrete_cp_inst @{type_name char} @{thm "perm_char_def"}
    1.57 +         |> discrete_pt_inst @{type_name nat} @{thm perm_nat_def}
    1.58 +         |> discrete_fs_inst @{type_name nat} @{thm perm_nat_def}
    1.59 +         |> discrete_cp_inst @{type_name nat} @{thm perm_nat_def}
    1.60 +         |> discrete_pt_inst @{type_name bool} @{thm perm_bool}
    1.61 +         |> discrete_fs_inst @{type_name bool} @{thm perm_bool}
    1.62 +         |> discrete_cp_inst @{type_name bool} @{thm perm_bool}
    1.63 +         |> discrete_pt_inst @{type_name int} @{thm perm_int_def}
    1.64 +         |> discrete_fs_inst @{type_name int} @{thm perm_int_def}
    1.65 +         |> discrete_cp_inst @{type_name int} @{thm perm_int_def}
    1.66 +         |> discrete_pt_inst @{type_name char} @{thm perm_char_def}
    1.67 +         |> discrete_fs_inst @{type_name char} @{thm perm_char_def}
    1.68 +         |> discrete_cp_inst @{type_name char} @{thm perm_char_def}
    1.69          end;
    1.70  
    1.71