src/Pure/Isar/context_rules.ML
changeset 15570 8d8c70b41bab
parent 15531 08c8dad8e399
child 15574 b1d1b5bfc464
     1.1 --- a/src/Pure/Isar/context_rules.ML	Thu Mar 03 09:22:35 2005 +0100
     1.2 +++ b/src/Pure/Isar/context_rules.ML	Thu Mar 03 12:43:01 2005 +0100
     1.3 @@ -112,8 +112,8 @@
     1.4  fun print_rules prt x (Rules {rules, ...}) =
     1.5    let
     1.6      fun prt_kind (i, b) =
     1.7 -      Pretty.big_list (the (assoc (kind_names, (i, b))) ^ ":")
     1.8 -        (mapfilter (fn (_, (k, th)) => if k = (i, b) then SOME (prt x th) else NONE)
     1.9 +      Pretty.big_list (valOf (assoc (kind_names, (i, b))) ^ ":")
    1.10 +        (List.mapPartial (fn (_, (k, th)) => if k = (i, b) then SOME (prt x th) else NONE)
    1.11            (sort (Int.compare o pairself fst) rules));
    1.12    in Pretty.writeln (Pretty.chunks (map prt_kind rule_kinds)) end;
    1.13  
    1.14 @@ -136,7 +136,7 @@
    1.15        val rules = gen_merge_lists' (fn ((_, (k1, th1)), (_, (k2, th2))) =>
    1.16            k1 = k2 andalso Drule.eq_thm_prop (th1, th2)) rules1 rules2;
    1.17        val next = ~ (length rules);
    1.18 -      val netpairs = foldl (fn (nps, (n, (w, ((i, b), th)))) =>
    1.19 +      val netpairs = Library.foldl (fn (nps, (n, (w, ((i, b), th)))) =>
    1.20            map_nth_elem i (curry insert_tagged_brl ((w, n), (b, th))) nps)
    1.21          (empty_netpairs, next upto ~1 ~~ rules);
    1.22      in make_rules (next - 1) rules netpairs wrappers end;
    1.23 @@ -203,7 +203,7 @@
    1.24  
    1.25  fun gen_wrap which ctxt =
    1.26    let val Rules {wrappers, ...} = LocalRules.get ctxt
    1.27 -  in fn tac => foldr (fn ((w, _), t) => w t) (which wrappers, tac) end;
    1.28 +  in fn tac => Library.foldr (fn ((w, _), t) => w t) (which wrappers, tac) end;
    1.29  
    1.30  val Swrap = gen_wrap #1;
    1.31  val wrap = gen_wrap #2;