src/Pure/Thy/present.ML
changeset 52551 f4fe75218cec
parent 52549 802576856527
child 52743 a7d69a11f395
     1.1 --- a/src/Pure/Thy/present.ML	Sun Jul 07 18:43:14 2013 +0200
     1.2 +++ b/src/Pure/Thy/present.ML	Sun Jul 07 18:50:16 2013 +0200
     1.3 @@ -4,15 +4,10 @@
     1.4  Theory presentation: HTML, graph files, (PDF)LaTeX documents.
     1.5  *)
     1.6  
     1.7 -signature BASIC_PRESENT =
     1.8 -sig
     1.9 -  val no_document: ('a -> 'b) -> 'a -> 'b  (*not thread-safe!*)
    1.10 -end;
    1.11 -
    1.12  signature PRESENT =
    1.13  sig
    1.14 -  include BASIC_PRESENT
    1.15    val session_name: theory -> string
    1.16 +  val no_document: ('a -> 'b) -> 'a -> 'b  (*not thread-safe!*)
    1.17    val read_variant: string -> string * string
    1.18    val init: bool -> bool -> Path.T -> string -> bool -> string -> (string * string) list ->
    1.19      string * string -> bool * string -> bool -> theory list -> unit  (*not thread-safe!*)
    1.20 @@ -497,5 +492,3 @@
    1.21  
    1.22  end;
    1.23  
    1.24 -structure Basic_Present: BASIC_PRESENT = Present;
    1.25 -open Basic_Present;