--- a/src/Pure/Isar/isar_cmd.ML Thu Oct 21 18:47:33 1999 +0200
+++ b/src/Pure/Isar/isar_cmd.ML Thu Oct 21 18:59:01 1999 +0200
@@ -11,6 +11,7 @@
val init_toplevel: Toplevel.transition -> Toplevel.transition
val exit: Toplevel.transition -> Toplevel.transition
val quit: Toplevel.transition -> Toplevel.transition
+ val touch_child_thys: string -> Toplevel.transition -> Toplevel.transition
val touch_all_thys: Toplevel.transition -> Toplevel.transition
val touch_thy: string -> Toplevel.transition -> Toplevel.transition
val remove_thy: string -> Toplevel.transition -> Toplevel.transition
@@ -66,6 +67,7 @@
(* touch theories *)
+fun touch_child_thys name = Toplevel.imperative (fn () => ThyInfo.touch_child_thys name);
val touch_all_thys = Toplevel.imperative ThyInfo.touch_all_thys;
fun touch_thy name = Toplevel.imperative (fn () => ThyInfo.touch_thy name);
fun remove_thy name = Toplevel.imperative (fn () => ThyInfo.remove_thy name);