# HG changeset patch
# User wenzelm
# Date 1030439205 -7200
# Node ID 5825aef91ac569e7e3ef3052a9688fc56580d94b
# Parent  4813fdc0ef17f802ab21f89e29772fea89bd75b2
simplified results;

diff -r 4813fdc0ef17 -r 5825aef91ac5 src/Pure/Thy/html.ML
--- a/src/Pure/Thy/html.ML	Tue Aug 27 11:06:20 2002 +0200
+++ b/src/Pure/Thy/html.ML	Tue Aug 27 11:06:45 2002 +0200
@@ -34,10 +34,7 @@
     (Url.T option * Url.T * bool option) list -> text -> text
   val end_theory: text
   val ml_file: Url.T -> string -> text
-  val multi_result: string * (string * thm list) list -> text
-  val results: string -> string -> thm list -> text
-  val theorem: string -> thm -> text
-  val theorems: string -> thm list -> text
+  val results: string -> (string * thm list) list -> text
   val chapter: string -> text
   val section: string -> text
   val subsection: string -> text
@@ -277,14 +274,10 @@
 
 in
 
-fun results k a ths = para (cat_lines ((keyword k ^ thm_name a) :: map thm ths));
+fun result k (a, ths) = para (cat_lines ((keyword k ^ thm_name a) :: map thm ths));
 
-fun multi_result (_, []) = ""
-  | multi_result (k, ((a, ths) :: res)) =
-      cat_lines (results k a ths :: map (uncurry (results "and")) res);
-
-fun theorem a th = multi_result ("theorem", [(a, [th])]);
-val theorems = results "theorems";
+fun results _ [] = ""
+  | results k (res :: ress) = cat_lines (result k res :: map (result "and") ress);
 
 end;