src/Pure/Isar/calculation.ML
changeset 10008 61eb9f3aa92a
parent 9900 8035a13c61a0
child 10478 97247fd6f1f8
     1.1 --- a/src/Pure/Isar/calculation.ML	Sun Sep 17 22:19:02 2000 +0200
     1.2 +++ b/src/Pure/Isar/calculation.ML	Sun Sep 17 22:21:31 2000 +0200
     1.3 @@ -28,8 +28,8 @@
     1.4  
     1.5  (* theory data kind 'Isar/calculation' *)
     1.6  
     1.7 -fun print_rules rs = Pretty.writeln (Pretty.big_list "transitivity rules:"
     1.8 -  (map Display.pretty_thm (NetRules.rules rs)));
     1.9 +fun print_rules sg rs = Pretty.writeln (Pretty.big_list "transitivity rules:"
    1.10 +  (map (Display.pretty_thm_sg sg) (NetRules.rules rs)));
    1.11  
    1.12  structure GlobalCalculationArgs =
    1.13  struct
    1.14 @@ -40,7 +40,7 @@
    1.15    val copy = I;
    1.16    val prep_ext = I;
    1.17    val merge = NetRules.merge;
    1.18 -  fun print _ = print_rules;
    1.19 +  val print = print_rules;
    1.20  end;
    1.21  
    1.22  structure GlobalCalculation = TheoryDataFun(GlobalCalculationArgs);
    1.23 @@ -55,7 +55,7 @@
    1.24    type T = thm NetRules.T * (thm list * int) option;
    1.25  
    1.26    fun init thy = (GlobalCalculation.get thy, None);
    1.27 -  fun print _ (rs, _) = print_rules rs;
    1.28 +  fun print ctxt (rs, _) = print_rules (ProofContext.sign_of ctxt) rs;
    1.29  end;
    1.30  
    1.31  structure LocalCalculation = ProofDataFun(LocalCalculationArgs);