| changeset 33037 | b22e44496dc2 |
| parent 32683 | 7c1fe854ca6a |
| child 33038 | 8f9594c31de4 |
--- a/src/HOL/Tools/inductive_set.ML Tue Oct 20 13:37:56 2009 +0200 +++ b/src/HOL/Tools/inductive_set.ML Tue Oct 20 16:13:01 2009 +0200 @@ -209,7 +209,7 @@ (case optf of NONE => fs | SOME f => AList.update op = (u, the_default f - (Option.map (curry op inter f) (AList.lookup op = fs u))) fs)); + (Option.map (curry (gen_inter (op =)) f) (AList.lookup op = fs u))) fs)); (**************************************************************)