src/Pure/Thy/present.ML
changeset 52551 f4fe75218cec
parent 52549 802576856527
child 52743 a7d69a11f395
--- 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;