src/Pure/defs.ML
changeset 20668 00521d5e1838
parent 20390 c80247278cb6
child 24199 8be734b5f59f
     1.1 --- a/src/Pure/defs.ML	Thu Sep 21 19:04:43 2006 +0200
     1.2 +++ b/src/Pure/defs.ML	Thu Sep 21 19:04:49 2006 +0200
     1.3 @@ -140,12 +140,11 @@
     1.4        | SOME subst => SOME (map (apsnd (map subst)) rhs));
     1.5      fun reducts (d, Us) = get_first (reduct Us) (reducts_of defs d);
     1.6  
     1.7 -    fun add (NONE, dp) = insert (op =) dp
     1.8 -      | add (SOME dps, _) = fold (insert (op =)) dps;
     1.9      val reds = map (`reducts) deps;
    1.10      val deps' =
    1.11        if forall (is_none o #1) reds then NONE
    1.12 -      else SOME (fold_rev add reds []);
    1.13 +      else SOME (fold_rev
    1.14 +        (fn (NONE, dp) => insert (op =) dp | (SOME dps, _) => fold (insert (op =)) dps) reds []);
    1.15      val _ = forall (acyclic pp defs const) (the_default deps deps');
    1.16    in deps' end;
    1.17