--- a/src/HOL/Nominal/nominal_atoms.ML Tue Jan 15 16:19:21 2008 +0100
+++ b/src/HOL/Nominal/nominal_atoms.ML Tue Jan 15 16:19:23 2008 +0100
@@ -717,9 +717,9 @@
|> discrete_pt_inst "bool" @{thm "perm_bool"}
|> discrete_fs_inst "bool" @{thm "perm_bool"}
|> discrete_cp_inst "bool" @{thm "perm_bool"}
- |> discrete_pt_inst "IntDef.int" @{thm "perm_int_def"}
- |> discrete_fs_inst "IntDef.int" @{thm "perm_int_def"}
- |> discrete_cp_inst "IntDef.int" @{thm "perm_int_def"}
+ |> 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"}