src/Tools/WWW_Find/find_theorems.ML

 
 Simple find_theorems server.
 *)
 
 local
+
 val default_limit = 20;
-val thy_names = sort string_ord (ThyInfo.get_names ());
+val thy_names = sort string_ord (Thy_Info.get_names ());
 
 val find_theorems_url = "find_theorems";
 
 fun is_sorry thm =
   Thm.proof_of thm

           ERROR msg => Xhtml.write send (html_error msg)
         | e => Xhtml.write send (html_error ("Server error: " ^ exnMessage e));
     Xhtml.write_close send header
   end;
 in
+
 val () = show_question_marks := false;
 val () = ScgiServer.register (find_theorems_url, SOME Mime.html, find_theorems);
+
 end;