src/Pure/Isar/calculation.ML
changeset 12055 a9c44895cc8c
parent 12021 8809efda06d3
child 12123 739eba13e2cd
     1.1 --- a/src/Pure/Isar/calculation.ML	Mon Nov 05 20:58:28 2001 +0100
     1.2 +++ b/src/Pure/Isar/calculation.ML	Mon Nov 05 20:59:35 2001 +0100
     1.3 @@ -14,10 +14,12 @@
     1.4    val trans_del_global: theory attribute
     1.5    val trans_add_local: Proof.context attribute
     1.6    val trans_del_local: Proof.context attribute
     1.7 -  val also: thm list option -> (thm list -> unit) -> Proof.state -> Proof.state Seq.seq
     1.8 -  val finally: thm list option -> (thm list -> unit) -> Proof.state -> Proof.state Seq.seq
     1.9 -  val moreover: (thm list -> unit) -> Proof.state -> Proof.state
    1.10 -  val ultimately: (thm list -> unit) -> Proof.state -> Proof.state
    1.11 +  val also: thm list option -> (Proof.context -> thm list -> unit)
    1.12 +    -> Proof.state -> Proof.state Seq.seq
    1.13 +  val finally: thm list option -> (Proof.context -> thm list -> unit)
    1.14 +    -> Proof.state -> Proof.state Seq.seq
    1.15 +  val moreover: (Proof.context -> thm list -> unit) -> Proof.state -> Proof.state
    1.16 +  val ultimately: (Proof.context -> thm list -> unit) -> Proof.state -> Proof.state
    1.17    val setup: (theory -> theory) list
    1.18  end;
    1.19  
    1.20 @@ -28,8 +30,8 @@
    1.21  
    1.22  (* theory data kind 'Isar/calculation' *)
    1.23  
    1.24 -fun print_rules sg rs = Pretty.writeln (Pretty.big_list "transitivity rules:"
    1.25 -  (map (Display.pretty_thm_sg sg) (NetRules.rules rs)));
    1.26 +fun print_rules prt x rs =
    1.27 +  Pretty.writeln (Pretty.big_list "transitivity rules:" (map (prt x) (NetRules.rules rs)));
    1.28  
    1.29  structure GlobalCalculationArgs =
    1.30  struct
    1.31 @@ -40,7 +42,7 @@
    1.32    val copy = I;
    1.33    val prep_ext = I;
    1.34    val merge = NetRules.merge;
    1.35 -  val print = print_rules;
    1.36 +  val print = print_rules Display.pretty_thm_sg;
    1.37  end;
    1.38  
    1.39  structure GlobalCalculation = TheoryDataFun(GlobalCalculationArgs);
    1.40 @@ -55,7 +57,7 @@
    1.41    type T = thm NetRules.T * (thm list * int) option;
    1.42  
    1.43    fun init thy = (GlobalCalculation.get thy, None);
    1.44 -  fun print ctxt (rs, _) = print_rules (ProofContext.sign_of ctxt) rs;
    1.45 +  fun print ctxt (rs, _) = print_rules ProofContext.pretty_thm ctxt rs;
    1.46  end;
    1.47  
    1.48  structure LocalCalculation = ProofDataFun(LocalCalculationArgs);
    1.49 @@ -143,7 +145,8 @@
    1.50    in
    1.51      err_if state (initial andalso final) "No calculation yet";
    1.52      err_if state (initial andalso is_some opt_rules) "Initial calculation -- no rules to be given";
    1.53 -    calculations |> Seq.map (fn calc => (print calc; state |> maintain_calculation final calc))
    1.54 +    calculations |> Seq.map (fn calc => (print (Proof.context_of state) calc;
    1.55 +        state |> maintain_calculation final calc))
    1.56    end;
    1.57  
    1.58  fun also print = calculate false print;
    1.59 @@ -162,7 +165,7 @@
    1.60      val calc = thms @ facts;
    1.61    in
    1.62      err_if state (initial andalso final) "No calculation yet";
    1.63 -    print calc;
    1.64 +    print (Proof.context_of state) calc;
    1.65      state |> maintain_calculation final calc
    1.66    end;
    1.67