src/Pure/Isar/context_rules.ML
changeset 22846 fb79144af9a3
parent 22360 26ead7ed4f4b
child 23178 07ba6b58b3d2
     1.1 --- a/src/Pure/Isar/context_rules.ML	Sun May 06 21:50:17 2007 +0200
     1.2 +++ b/src/Pure/Isar/context_rules.ML	Mon May 07 00:49:59 2007 +0200
     1.3 @@ -94,9 +94,7 @@
     1.4  
     1.5  structure Rules = GenericDataFun
     1.6  (
     1.7 -  val name = "Pure/rules";
     1.8    type T = T;
     1.9 -
    1.10    val empty = make_rules ~1 [] empty_netpairs ([], []);
    1.11    val extend = I;
    1.12  
    1.13 @@ -112,20 +110,17 @@
    1.14            nth_map i (curry insert_tagged_brl ((w, n), (b, th))))
    1.15          (next upto ~1 ~~ rules) empty_netpairs;
    1.16      in make_rules (next - 1) rules netpairs wrappers end
    1.17 -
    1.18 -  fun print generic (Rules {rules, ...}) =
    1.19 -    let
    1.20 -      val ctxt = Context.proof_of generic;
    1.21 -      fun prt_kind (i, b) =
    1.22 -        Pretty.big_list ((the o AList.lookup (op =) kind_names) (i, b) ^ ":")
    1.23 -          (map_filter (fn (_, (k, th)) =>
    1.24 -              if k = (i, b) then SOME (ProofContext.pretty_thm ctxt th) else NONE)
    1.25 -            (sort (int_ord o pairself fst) rules));
    1.26 -    in Pretty.writeln (Pretty.chunks (map prt_kind rule_kinds)) end;
    1.27  );
    1.28  
    1.29 -val _ = Context.add_setup Rules.init;
    1.30 -val print_rules = Rules.print o Context.Proof;
    1.31 +fun print_rules ctxt =
    1.32 +  let
    1.33 +    val Rules {rules, ...} = Rules.get (Context.Proof ctxt);
    1.34 +    fun prt_kind (i, b) =
    1.35 +      Pretty.big_list ((the o AList.lookup (op =) kind_names) (i, b) ^ ":")
    1.36 +        (map_filter (fn (_, (k, th)) =>
    1.37 +            if k = (i, b) then SOME (ProofContext.pretty_thm ctxt th) else NONE)
    1.38 +          (sort (int_ord o pairself fst) rules));
    1.39 +  in Pretty.writeln (Pretty.chunks (map prt_kind rule_kinds)) end;
    1.40  
    1.41  
    1.42  (* access data *)