changeset 18964 | 67f572e03236 |
parent 18952 | 0388d0b0f3d5 |
child 19018 | 88b4979193d8 |
--- a/src/Pure/Isar/locale.ML Tue Feb 07 08:47:43 2006 +0100 +++ b/src/Pure/Isar/locale.ML Tue Feb 07 19:56:45 2006 +0100 @@ -675,7 +675,7 @@ fun rename_parms top ren ((name, ps), (parms, mode)) = let val ps' = map (Element.rename ren) ps in - (case duplicates ps' of + (case duplicates (op =) ps' of [] => ((name, ps'), if top then (map (Element.rename ren) parms, map_mode (map (fn (t, th) =>