1.1 --- a/src/Pure/Isar/method.ML	Sun Sep 17 22:19:02 2000 +0200
     1.2 +++ b/src/Pure/Isar/method.ML	Sun Sep 17 22:21:31 2000 +0200
     1.3 @@ -127,11 +127,14 @@
     1.4  
     1.5  (** global and local rule data **)
     1.6  
     1.7 -fun prt_rules kind ths =
     1.8 -  Pretty.writeln (Pretty.big_list ("standard " ^ kind ^ " rules:") (map Display.pretty_thm ths));
     1.9 -
    1.10 -fun print_rules (intro, elim) =
    1.11 -  (prt_rules "introduction" intro; prt_rules "elimination" elim);
    1.12 +local
    1.13 +  fun prt_rules kind sg ths =
    1.14 +    Pretty.writeln (Pretty.big_list ("standard " ^ kind ^ " rules:")
    1.15 +      (map (Display.pretty_thm_sg sg) ths));
    1.16 +in
    1.17 +  fun print_rules sg (intro, elim) =
    1.18 +    (prt_rules "introduction" sg intro; prt_rules "elimination" sg elim);
    1.19 +end;
    1.20  
    1.21  
    1.22  (* theory data kind 'Isar/rules' *)
    1.23 @@ -146,7 +149,7 @@
    1.24    val prep_ext = I;
    1.25    fun merge ((intro1, elim1), (intro2, elim2)) =
    1.26      (Drule.merge_rules (intro1, intro2), Drule.merge_rules (elim1, elim2));
    1.27 -  fun print _ = print_rules;
    1.28 +  val print = print_rules;
    1.29  end;
    1.30  
    1.31  structure GlobalRules = TheoryDataFun(GlobalRulesArgs);
    1.32 @@ -161,7 +164,7 @@
    1.33    type T = thm list * thm list;
    1.34  
    1.35    val init = GlobalRules.get;
    1.36 -  fun print _ = print_rules;
    1.37 +  val print = print_rules o ProofContext.sign_of;
    1.38  end;
    1.39  
    1.40  structure LocalRules = ProofDataFun(LocalRulesArgs);