simplified results;
authorwenzelm
Tue Aug 27 11:06:45 2002 +0200 (2002-08-27)
changeset 135315825aef91ac5
parent 13530 4813fdc0ef17
child 13532 131bb248504d
simplified results;
src/Pure/Thy/html.ML
     1.1 --- a/src/Pure/Thy/html.ML	Tue Aug 27 11:06:20 2002 +0200
     1.2 +++ b/src/Pure/Thy/html.ML	Tue Aug 27 11:06:45 2002 +0200
     1.3 @@ -34,10 +34,7 @@
     1.4      (Url.T option * Url.T * bool option) list -> text -> text
     1.5    val end_theory: text
     1.6    val ml_file: Url.T -> string -> text
     1.7 -  val multi_result: string * (string * thm list) list -> text
     1.8 -  val results: string -> string -> thm list -> text
     1.9 -  val theorem: string -> thm -> text
    1.10 -  val theorems: string -> thm list -> text
    1.11 +  val results: string -> (string * thm list) list -> text
    1.12    val chapter: string -> text
    1.13    val section: string -> text
    1.14    val subsection: string -> text
    1.15 @@ -277,14 +274,10 @@
    1.16  
    1.17  in
    1.18  
    1.19 -fun results k a ths = para (cat_lines ((keyword k ^ thm_name a) :: map thm ths));
    1.20 +fun result k (a, ths) = para (cat_lines ((keyword k ^ thm_name a) :: map thm ths));
    1.21  
    1.22 -fun multi_result (_, []) = ""
    1.23 -  | multi_result (k, ((a, ths) :: res)) =
    1.24 -      cat_lines (results k a ths :: map (uncurry (results "and")) res);
    1.25 -
    1.26 -fun theorem a th = multi_result ("theorem", [(a, [th])]);
    1.27 -val theorems = results "theorems";
    1.28 +fun results _ [] = ""
    1.29 +  | results k (res :: ress) = cat_lines (result k res :: map (result "and") ress);
    1.30  
    1.31  end;
    1.32