diff -r 1ec1567c1307 -r f8ce7b832598 src/Pure/Thy/browser_info.ML
--- a/src/Pure/Thy/browser_info.ML	Wed Sep 01 21:06:27 1999 +0200
+++ b/src/Pure/Thy/browser_info.ML	Wed Sep 01 21:06:57 1999 +0200
@@ -19,6 +19,7 @@
   val begin_theory: string -> string list -> (Path.T * bool) list -> theory -> theory
   val end_theory: string -> unit
   val theorem: string -> thm -> unit
+  val theorems: string -> thm list -> unit
   val setup: (theory -> theory) list
 end;
 
@@ -319,8 +320,8 @@
   let
     val parents = map (parent_link remote_path path) raw_parents;
     val ml_path = ThyLoad.ml_path name;
-    val files = orig_files @		(* FIXME improve!? *)
-      (if is_some (ThyLoad.check_file ml_path) then [(ml_path, true)] else []);
+    val files = map (apsnd Some) orig_files @
+      (if is_some (ThyLoad.check_file ml_path) then [(ml_path, None)] else []);
 
     fun prep_file (raw_path, loadit) =
       (case ThyLoad.check_file raw_path of
@@ -359,6 +360,7 @@
 fun end_theory _ = ();
 
 fun theorem name thm = with_session () (fn _ => with_context add_html (HTML.theorem name thm));
+fun theorems name thms = with_session () (fn _ => with_context add_html (HTML.theorems name thms));
 fun section s = with_session () (fn _ => with_context add_html (HTML.section s));