# HG changeset patch
# User wenzelm
# Date 1373215816 -7200
# Node ID f4fe75218cec5dc8b12fcf2af11b0162a7737f95
# Parent  09e52d4a850ade6f43b37e14d44625cea8c114dd
tuned signature;

diff -r 09e52d4a850a -r f4fe75218cec src/Pure/Thy/present.ML
--- a/src/Pure/Thy/present.ML	Sun Jul 07 18:43:14 2013 +0200
+++ b/src/Pure/Thy/present.ML	Sun Jul 07 18:50:16 2013 +0200
@@ -4,15 +4,10 @@
 Theory presentation: HTML, graph files, (PDF)LaTeX documents.
 *)
 
-signature BASIC_PRESENT =
-sig
-  val no_document: ('a -> 'b) -> 'a -> 'b  (*not thread-safe!*)
-end;
-
 signature PRESENT =
 sig
-  include BASIC_PRESENT
   val session_name: theory -> string
+  val no_document: ('a -> 'b) -> 'a -> 'b  (*not thread-safe!*)
   val read_variant: string -> string * string
   val init: bool -> bool -> Path.T -> string -> bool -> string -> (string * string) list ->
     string * string -> bool * string -> bool -> theory list -> unit  (*not thread-safe!*)
@@ -497,5 +492,3 @@
 
 end;
 
-structure Basic_Present: BASIC_PRESENT = Present;
-open Basic_Present;