--- a/src/Pure/Thy/present.ML Wed Oct 06 21:32:52 1999 +0200
+++ b/src/Pure/Thy/present.ML Thu Oct 07 11:34:46 1999 +0200
@@ -29,6 +29,7 @@
val subsection: string -> unit
val subsubsection: string -> unit
val setup: (theory -> theory) list
+ val get_info: theory -> {session: string list, is_local: bool}
end;
structure Present: PRESENT =
@@ -66,7 +67,7 @@
val empty = {session = [], is_local = false};
val copy = I;
- val prep_ext = I;
+ fun prep_ext _ = empty;
fun merge _ = empty;
fun print _ _ = ();
end;