src/Pure/Isar/isar_thy.ML
changeset 6531 8064ed198068
parent 6501 392333eb31cb
child 6552 28553eba1913
     1.1 --- a/src/Pure/Isar/isar_thy.ML	Tue Apr 27 15:13:58 1999 +0200
     1.2 +++ b/src/Pure/Isar/isar_thy.ML	Tue Apr 27 15:14:22 1999 +0200
     1.3 @@ -227,10 +227,15 @@
     1.4  
     1.5  (* local endings *)
     1.6  
     1.7 -val local_qed = Toplevel.proof o ProofHistory.applys_close o Method.local_qed;
     1.8 -val local_terminal_proof = Toplevel.proof o ProofHistory.applys_close o Method.local_terminal_proof;
     1.9 -val local_immediate_proof = Toplevel.proof (ProofHistory.applys_close Method.local_immediate_proof);
    1.10 -val local_default_proof = Toplevel.proof (ProofHistory.applys_close Method.local_default_proof);
    1.11 +(* FIXME
    1.12 +val print_proof = Toplevel.print oo Toplevel.proof;
    1.13 +*)
    1.14 +val print_proof = Toplevel.proof;
    1.15 +
    1.16 +val local_qed = print_proof o ProofHistory.applys_close o Method.local_qed;
    1.17 +val local_terminal_proof = print_proof o ProofHistory.applys_close o Method.local_terminal_proof;
    1.18 +val local_immediate_proof = print_proof (ProofHistory.applys_close Method.local_immediate_proof);
    1.19 +val local_default_proof = print_proof (ProofHistory.applys_close Method.local_default_proof);
    1.20  
    1.21  
    1.22  (* global endings *)
    1.23 @@ -241,7 +246,7 @@
    1.24    let
    1.25      val state = ProofHistory.current prf;
    1.26      val _ = if Proof.at_bottom state then () else raise Toplevel.UNDEF;
    1.27 -    val (thy, (kind, name, thm)) = finish state;
    1.28 +    val (thy, {kind, name, thm}) = finish state;
    1.29  
    1.30      val prt_result = Pretty.block
    1.31        [Pretty.str (kind ^ " " ^ name ^ ":"), Pretty.fbrk, Display.pretty_thm thm];