src/Pure/Isar/runtime.ML
changeset 62889 99c7f31615c2
parent 62878 1cec457e0a03
child 65948 de7888573ed7
     1.1 --- a/src/Pure/Isar/runtime.ML	Wed Apr 06 14:08:57 2016 +0200
     1.2 +++ b/src/Pure/Isar/runtime.ML	Wed Apr 06 16:33:33 2016 +0200
     1.3 @@ -54,7 +54,7 @@
     1.4    | exn_context (SOME ctxt) exn = if Exn.is_interrupt exn then exn else CONTEXT (ctxt, exn);
     1.5  
     1.6  fun thread_context exn =
     1.7 -  exn_context (Option.map Context.proof_of (Context.thread_data ())) exn;
     1.8 +  exn_context (Option.map Context.proof_of (Context.get_generic_context ())) exn;
     1.9  
    1.10  
    1.11  (* exn_message *)
    1.12 @@ -202,7 +202,7 @@
    1.13      else
    1.14        let
    1.15          val opt_ctxt =
    1.16 -          (case Context.thread_data () of
    1.17 +          (case Context.get_generic_context () of
    1.18              NONE => NONE
    1.19            | SOME context => try Context.proof_of context);
    1.20          val _ = output_exn (exn_context opt_ctxt exn);