# HG changeset patch
# User wenzelm
# Date 925218862 -7200
# Node ID 8064ed19806801d268409efb125777f1f7edaa5e
# Parent  473305b71b741396b573b7149d0e025c403ac125
tuned;

diff -r 473305b71b74 -r 8064ed198068 src/Pure/Isar/isar_thy.ML
--- a/src/Pure/Isar/isar_thy.ML	Tue Apr 27 15:13:58 1999 +0200
+++ b/src/Pure/Isar/isar_thy.ML	Tue Apr 27 15:14:22 1999 +0200
@@ -227,10 +227,15 @@
 
 (* local endings *)
 
-val local_qed = Toplevel.proof o ProofHistory.applys_close o Method.local_qed;
-val local_terminal_proof = Toplevel.proof o ProofHistory.applys_close o Method.local_terminal_proof;
-val local_immediate_proof = Toplevel.proof (ProofHistory.applys_close Method.local_immediate_proof);
-val local_default_proof = Toplevel.proof (ProofHistory.applys_close Method.local_default_proof);
+(* FIXME
+val print_proof = Toplevel.print oo Toplevel.proof;
+*)
+val print_proof = Toplevel.proof;
+
+val local_qed = print_proof o ProofHistory.applys_close o Method.local_qed;
+val local_terminal_proof = print_proof o ProofHistory.applys_close o Method.local_terminal_proof;
+val local_immediate_proof = print_proof (ProofHistory.applys_close Method.local_immediate_proof);
+val local_default_proof = print_proof (ProofHistory.applys_close Method.local_default_proof);
 
 
 (* global endings *)
@@ -241,7 +246,7 @@
   let
     val state = ProofHistory.current prf;
     val _ = if Proof.at_bottom state then () else raise Toplevel.UNDEF;
-    val (thy, (kind, name, thm)) = finish state;
+    val (thy, {kind, name, thm}) = finish state;
 
     val prt_result = Pretty.block
       [Pretty.str (kind ^ " " ^ name ^ ":"), Pretty.fbrk, Display.pretty_thm thm];