src/HOL/Tools/Function/fundef_lib.ML
changeset 32683 7c1fe854ca6a
parent 32197 bc341bbe4417
child 33040 cffdb7b28498
     1.1 --- a/src/HOL/Tools/Function/fundef_lib.ML	Fri Sep 18 14:09:38 2009 +0200
     1.2 +++ b/src/HOL/Tools/Function/fundef_lib.ML	Sat Sep 19 07:38:03 2009 +0200
     1.3 @@ -170,7 +170,7 @@
     1.4   end
     1.5  
     1.6  (* instance for unions *)
     1.7 -fun regroup_union_conv t = regroup_conv @{const_name Set.empty} @{const_name Set.union}
     1.8 +fun regroup_union_conv t = regroup_conv @{const_name Set.empty} @{const_name Lattices.sup}
     1.9    (map (fn t => t RS eq_reflection) (@{thms Un_ac} @
    1.10                                       @{thms Un_empty_right} @
    1.11                                       @{thms Un_empty_left})) t