# HG changeset patch
# User berghofe
# Date 939288886 -7200
# Node ID fdf7c941a22b5300a4627ee1f939caaea3b03c06
# Parent  c98d705380330e902576897fb442f20ff0414b60
Exported function get_info.

diff -r c98d70538033 -r fdf7c941a22b src/Pure/Thy/present.ML
--- 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;