src/Pure/Thy/present.ML
changeset 7763 fdf7c941a22b
parent 7757 b2538dccc21e
child 7769 700439dc581e
--- 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;