# HG changeset patch # User haftmann # Date 1241690536 -7200 # Node ID 45c085c7efc643a30d08e8286b70d681208492bf # Parent 9f151b0965333bcd828ec480791f66ef5a2fd827 explicit type_name antiquotations diff -r 9f151b096533 -r 45c085c7efc6 src/HOL/Nominal/nominal_atoms.ML --- a/src/HOL/Nominal/nominal_atoms.ML Thu May 07 12:02:15 2009 +0200 +++ b/src/HOL/Nominal/nominal_atoms.ML Thu May 07 12:02:16 2009 +0200 @@ -732,18 +732,18 @@ in thy26 - |> discrete_pt_inst "nat" @{thm "perm_nat_def"} - |> discrete_fs_inst "nat" @{thm "perm_nat_def"} - |> discrete_cp_inst "nat" @{thm "perm_nat_def"} - |> discrete_pt_inst "bool" @{thm "perm_bool"} - |> discrete_fs_inst "bool" @{thm "perm_bool"} - |> discrete_cp_inst "bool" @{thm "perm_bool"} - |> discrete_pt_inst @{type_name "Int.int"} @{thm "perm_int_def"} - |> discrete_fs_inst @{type_name "Int.int"} @{thm "perm_int_def"} - |> discrete_cp_inst @{type_name "Int.int"} @{thm "perm_int_def"} - |> discrete_pt_inst "List.char" @{thm "perm_char_def"} - |> discrete_fs_inst "List.char" @{thm "perm_char_def"} - |> discrete_cp_inst "List.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;