src/HOL/Nominal/nominal_atoms.ML
changeset 25919 8b1c0d434824
parent 25557 ea6b11021e79
child 26090 ec111fa4f8c5
     1.1 --- a/src/HOL/Nominal/nominal_atoms.ML	Tue Jan 15 16:19:21 2008 +0100
     1.2 +++ b/src/HOL/Nominal/nominal_atoms.ML	Tue Jan 15 16:19:23 2008 +0100
     1.3 @@ -717,9 +717,9 @@
     1.4           |> discrete_pt_inst "bool" @{thm "perm_bool"}
     1.5           |> discrete_fs_inst "bool" @{thm "perm_bool"}
     1.6           |> discrete_cp_inst "bool" @{thm "perm_bool"}
     1.7 -         |> discrete_pt_inst "IntDef.int" @{thm "perm_int_def"}
     1.8 -         |> discrete_fs_inst "IntDef.int" @{thm "perm_int_def"}
     1.9 -         |> discrete_cp_inst "IntDef.int" @{thm "perm_int_def"}
    1.10 +         |> discrete_pt_inst @{type_name "Int.int"} @{thm "perm_int_def"}
    1.11 +         |> discrete_fs_inst @{type_name "Int.int"} @{thm "perm_int_def"}
    1.12 +         |> discrete_cp_inst @{type_name "Int.int"} @{thm "perm_int_def"}
    1.13           |> discrete_pt_inst "List.char" @{thm "perm_char_def"}
    1.14           |> discrete_fs_inst "List.char" @{thm "perm_char_def"}
    1.15           |> discrete_cp_inst "List.char" @{thm "perm_char_def"}