changeset 44169 | bdcc11b2fdc8 |
parent 44080 | 53d95b52954c |
child 46909 | 3c73a121a387 |
--- a/src/HOL/HOLCF/Tools/domaindef.ML Fri Aug 12 07:13:12 2011 -0700 +++ b/src/HOL/HOLCF/Tools/domaindef.ML Fri Aug 12 07:18:28 2011 -0700 @@ -109,7 +109,7 @@ |> the_default (Binding.prefix_name "Rep_" name, Binding.prefix_name "Abs_" name) (*set*) - val set = @{term "defl_set :: udom defl => udom => bool"} $ defl + val set = @{term "defl_set :: udom defl => udom set"} $ defl (*pcpodef*) val tac1 = rtac @{thm defl_set_bottom} 1