src/Pure/Isar/local_defs.ML
changeset 22846 fb79144af9a3
parent 22691 290454649b8c
child 22900 f8a7c10e1bd0
     1.1 --- a/src/Pure/Isar/local_defs.ML	Sun May 06 21:50:17 2007 +0200
     1.2 +++ b/src/Pure/Isar/local_defs.ML	Mon May 07 00:49:59 2007 +0200
     1.3 @@ -147,19 +147,15 @@
     1.4  
     1.5  structure Rules = GenericDataFun
     1.6  (
     1.7 -  val name = "Pure/derived_defs";
     1.8    type T = thm list;
     1.9    val empty = []
    1.10    val extend = I;
    1.11    fun merge _ = Drule.merge_rules;
    1.12 -  fun print context rules =
    1.13 -    Pretty.writeln (Pretty.big_list "definitional transformations:"
    1.14 -      (map (ProofContext.pretty_thm (Context.proof_of context)) rules));
    1.15  );
    1.16  
    1.17 -val _ = Context.add_setup Rules.init;
    1.18 -
    1.19 -val print_rules = Rules.print o Context.Proof;
    1.20 +fun print_rules ctxt =
    1.21 +  Pretty.writeln (Pretty.big_list "definitional transformations:"
    1.22 +    (map (ProofContext.pretty_thm ctxt) (Rules.get (Context.Proof ctxt))));
    1.23  
    1.24  val defn_add = Thm.declaration_attribute (Rules.map o Drule.add_rule);
    1.25  val defn_del = Thm.declaration_attribute (Rules.map o Drule.del_rule);