equal
deleted
inserted
replaced
325 |
325 |
326 fun mapping add_names f t = |
326 fun mapping add_names f t = |
327 let |
327 let |
328 fun f' x = let val y = f x in if x = y then NONE else SOME (x, y) end; |
328 fun f' x = let val y = f x in if x = y then NONE else SOME (x, y) end; |
329 val tab = List.mapPartial f' (add_names (t, [])); |
329 val tab = List.mapPartial f' (add_names (t, [])); |
330 fun get x = if_none (assoc_string (tab, x)) x; |
330 fun get x = if_none (AList.lookup (op =) tab x) x; |
331 in get end; |
331 in get end; |
332 |
332 |
333 fun typ_mapping f g thy T = |
333 fun typ_mapping f g thy T = |
334 T |> Term.map_typ |
334 T |> Term.map_typ |
335 (mapping add_typ_classes (f thy) T) |
335 (mapping add_typ_classes (f thy) T) |