1.1 --- a/src/Pure/Thy/present.ML	Fri Jan 19 22:08:31 2007 +0100
     1.2 +++ b/src/Pure/Thy/present.ML	Fri Jan 19 22:08:32 2007 +0100
     1.3 @@ -245,7 +245,7 @@
     1.4  val session_info = ref (NONE: session_info option);
     1.5  
     1.6  fun with_session x f = (case ! session_info of NONE => x | SOME info => f info);
     1.7 -fun with_context f = f (Context.theory_name (Context.the_context ()));
     1.8 +fun with_context f = f (Context.theory_name (ML_Context.the_context ()));
     1.9  
    1.10  
    1.11  
    1.12 @@ -504,10 +504,11 @@
    1.13  
    1.14  fun results k xs =
    1.15   (List.app (fn f => (try (fn () => f k xs) (); ())) (! hooks);
    1.16 -  with_session () (fn _ => with_context add_html (HTML.results k xs)));
    1.17 +  with_session () (fn _ => with_context add_html
    1.18 +    (HTML.results (ML_Context.the_local_context ()) k xs)));
    1.19  
    1.20 -fun theorem a th = results "theorem" [(a, [th])];
    1.21 -fun theorems a ths = results "theorems" [(a, ths)];
    1.22 +fun theorem a th = results Thm.theoremK [(a, [th])];
    1.23 +fun theorems a ths = results Thm.theoremK [(a, ths)];
    1.24  fun chapter s = with_session () (fn _ => with_context add_html (HTML.chapter s));
    1.25  fun section s = with_session () (fn _ => with_context add_html (HTML.section s));
    1.26  fun subsection s = with_session () (fn _ => with_context add_html (HTML.subsection s));