# HG changeset patch # User panny # Date 1377767967 -7200 # Node ID 3c26a7042d8e61ad6c228a21047911b4df3ace03 # Parent 876ce6767d6801fd02577056866d461591973d2d removed outdated comments diff -r 876ce6767d68 -r 3c26a7042d8e src/HOL/BNF/Tools/bnf_def.ML --- a/src/HOL/BNF/Tools/bnf_def.ML Thu Aug 29 10:08:55 2013 +0200 +++ b/src/HOL/BNF/Tools/bnf_def.ML Thu Aug 29 11:19:27 2013 +0200 @@ -292,10 +292,10 @@ name: binding, T: typ, live: int, - lives: typ list, (*source type variables of map, only for composition*) - lives': typ list, (*target type variables of map, only for composition*) + lives: typ list, (*source type variables of map*) + lives': typ list, (*target type variables of map*) dead: int, - deads: typ list, (*only for composition*) + deads: typ list, map: term, sets: term list, bd: term,