src/Pure/proofterm.ML
changeset 43326 47cf4bc789aa
parent 43324 2b47822868e4
child 43329 84472e198515
     1.1 --- a/src/Pure/proofterm.ML	Thu Jun 09 17:46:25 2011 +0200
     1.2 +++ b/src/Pure/proofterm.ML	Thu Jun 09 17:51:49 2011 +0200
     1.3 @@ -657,7 +657,7 @@
     1.4        (fn TFree v => if member (op =) fixed v then I else insert (op =) v | _ => I)) t [];
     1.5      val used = Name.context
     1.6        |> fold_types (fold_atyps (fn TVar ((a, _), _) => Name.declare a | _ => I)) t;
     1.7 -    val fmap = fs ~~ #1 (Name.variants (map fst fs) used);
     1.8 +    val fmap = fs ~~ #1 (fold_map Name.variant (map fst fs) used);
     1.9      fun thaw (f as (a, S)) =
    1.10        (case AList.lookup (op =) fmap f of
    1.11          NONE => TFree f