src/Pure/Isar/context_rules.ML
changeset 19473 d87a8838afa4
parent 19046 bc5c6c9b114e
child 19482 9f11af8f7ef9
     1.1 --- a/src/Pure/Isar/context_rules.ML	Wed Apr 26 20:34:11 2006 +0200
     1.2 +++ b/src/Pure/Isar/context_rules.ML	Wed Apr 26 22:38:05 2006 +0200
     1.3 @@ -108,9 +108,9 @@
     1.4        val rules = Library.merge (fn ((_, (k1, th1)), (_, (k2, th2))) =>
     1.5            k1 = k2 andalso Drule.eq_thm_prop (th1, th2)) (rules1, rules2);
     1.6        val next = ~ (length rules);
     1.7 -      val netpairs = Library.foldl (fn (nps, (n, (w, ((i, b), th)))) =>
     1.8 -          nth_map i (curry insert_tagged_brl ((w, n), (b, th))) nps)
     1.9 -        (empty_netpairs, next upto ~1 ~~ rules);
    1.10 +      val netpairs = fold (fn (n, (w, ((i, b), th))) =>
    1.11 +          nth_map i (curry insert_tagged_brl ((w, n), (b, th))))
    1.12 +        (next upto ~1 ~~ rules) empty_netpairs;
    1.13      in make_rules (next - 1) rules netpairs wrappers end
    1.14  
    1.15    fun print generic (Rules {rules, ...}) =