# HG changeset patch
# User wenzelm
# Date 1224762748 -7200
# Node ID 0baf1d9c6780533fa3600d177cbbe731b1a23d7c
# Parent  ed6681dd35d8b58f3f7743a372d3b90ce0aec8da
adapted Susp.peek;

diff -r ed6681dd35d8 -r 0baf1d9c6780 src/Pure/Isar/code.ML
--- a/src/Pure/Isar/code.ML	Thu Oct 23 13:52:27 2008 +0200
+++ b/src/Pure/Isar/code.ML	Thu Oct 23 13:52:28 2008 +0200
@@ -118,12 +118,12 @@
 (* defining equations with linear flag, default flag and lazy theorems *)
 
 fun pretty_lthms ctxt r = case Susp.peek r
- of SOME thms => map (ProofContext.pretty_thm ctxt o fst) thms
+ of SOME thms => map (ProofContext.pretty_thm ctxt o fst) (Exn.release thms)
   | NONE => [Pretty.str "[...]"];
 
 fun certificate thy f r =
   case Susp.peek r
-   of SOME thms => (Susp.value o f thy) thms
+   of SOME thms => (Susp.value o f thy) (Exn.release thms)
     | NONE => let
         val thy_ref = Theory.check_thy thy;
       in Susp.delay (fn () => (f (Theory.deref thy_ref) o Susp.force) r) end;
diff -r ed6681dd35d8 -r 0baf1d9c6780 src/Pure/ML-Systems/install_pp_polyml.ML
--- a/src/Pure/ML-Systems/install_pp_polyml.ML	Thu Oct 23 13:52:27 2008 +0200
+++ b/src/Pure/ML-Systems/install_pp_polyml.ML	Thu Oct 23 13:52:28 2008 +0200
@@ -13,4 +13,6 @@
 install_pp (fn (str, _, _, _) => fn depth => fn (print: 'a * int -> unit) => fn (x: 'a Susp.T) =>
   (case Susp.peek x of
     NONE => str "<delayed>"
-  | SOME y => print (y, depth)));
+  | SOME (Exn.Exn _) => str "<failed>"
+  | SOME (Exn.Result y) => print (y, depth)));
+