1.1 --- a/src/Pure/Isar/code.ML	Thu Oct 23 13:52:27 2008 +0200
     1.2 +++ b/src/Pure/Isar/code.ML	Thu Oct 23 13:52:28 2008 +0200
     1.3 @@ -118,12 +118,12 @@
     1.4  (* defining equations with linear flag, default flag and lazy theorems *)
     1.5  
     1.6  fun pretty_lthms ctxt r = case Susp.peek r
     1.7 - of SOME thms => map (ProofContext.pretty_thm ctxt o fst) thms
     1.8 + of SOME thms => map (ProofContext.pretty_thm ctxt o fst) (Exn.release thms)
     1.9    | NONE => [Pretty.str "[...]"];
    1.10  
    1.11  fun certificate thy f r =
    1.12    case Susp.peek r
    1.13 -   of SOME thms => (Susp.value o f thy) thms
    1.14 +   of SOME thms => (Susp.value o f thy) (Exn.release thms)
    1.15      | NONE => let
    1.16          val thy_ref = Theory.check_thy thy;
    1.17        in Susp.delay (fn () => (f (Theory.deref thy_ref) o Susp.force) r) end;