# 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;