src/Pure/Isar/isar_thy.ML
changeset 7417 70c1d3eac214
parent 7353 b5a5abea1559
child 7476 85c8be727fdb
     1.1 --- a/src/Pure/Isar/isar_thy.ML	Wed Sep 01 21:16:23 1999 +0200
     1.2 +++ b/src/Pure/Isar/isar_thy.ML	Wed Sep 01 21:17:03 1999 +0200
     1.3 @@ -71,8 +71,8 @@
     1.4      -> ProofHistory.T -> ProofHistory.T
     1.5    val chain: Comment.text -> ProofHistory.T -> ProofHistory.T
     1.6    val export_chain: Comment.text -> ProofHistory.T -> ProofHistory.T
     1.7 -  val fix: (string * string option) list * Comment.text -> ProofHistory.T -> ProofHistory.T
     1.8 -  val fix_i: (string * typ) list * Comment.text -> ProofHistory.T -> ProofHistory.T
     1.9 +  val fix: ((string list * string option) * Comment.text) list -> ProofHistory.T -> ProofHistory.T
    1.10 +  val fix_i: ((string list * typ) * Comment.text) list -> ProofHistory.T -> ProofHistory.T
    1.11    val match_bind: ((string list * string) * Comment.text) list -> ProofHistory.T -> ProofHistory.T
    1.12    val match_bind_i: ((term list * term) * Comment.text) list -> ProofHistory.T -> ProofHistory.T
    1.13    val theorem: (bstring * Args.src list * (string * (string list * string list)))
    1.14 @@ -265,8 +265,8 @@
    1.15  
    1.16  (* context *)
    1.17  
    1.18 -val fix = ProofHistory.apply o Proof.fix o Comment.ignore;
    1.19 -val fix_i = ProofHistory.apply o Proof.fix_i o Comment.ignore;
    1.20 +val fix = ProofHistory.apply o Proof.fix o map Comment.ignore;
    1.21 +val fix_i = ProofHistory.apply o Proof.fix_i o map Comment.ignore;
    1.22  val match_bind = ProofHistory.apply o Proof.match_bind o map Comment.ignore;
    1.23  val match_bind_i = ProofHistory.apply o Proof.match_bind_i o map Comment.ignore;
    1.24  
    1.25 @@ -396,8 +396,8 @@
    1.26  
    1.27  local
    1.28  
    1.29 -fun cond_print_calc int thm =
    1.30 -  if int then Pretty.writeln (Pretty.big_list "calculation:" [Proof.pretty_thm thm])
    1.31 +fun cond_print_calc int thms =
    1.32 +  if int then Pretty.writeln (Pretty.big_list "calculation:" (map Proof.pretty_thm thms))
    1.33    else ();
    1.34  
    1.35  fun proof''' f = Toplevel.proof' (f o cond_print_calc);