# HG changeset patch
# User wenzelm
# Date 1279832298 -7200
# Node ID 050ca02c6dfcdeb27cd18f8ffbc42179e19bc9db
# Parent  1d812ff95a14b2905a8678cfe46bb29f794ece13
eliminated some unused Thy_Info operations;

diff -r 1d812ff95a14 -r 050ca02c6dfc src/Pure/Thy/thy_info.ML
--- a/src/Pure/Thy/thy_info.ML	Thu Jul 22 22:50:35 2010 +0200
+++ b/src/Pure/Thy/thy_info.ML	Thu Jul 22 22:58:18 2010 +0200
@@ -8,7 +8,6 @@
 signature THY_INFO =
 sig
   datatype action = Update | Outdate | Remove
-  val str_of_action: action -> string
   val add_hook: (action -> string -> unit) -> unit
   val get_names: unit -> string list
   val known_thy: string -> bool
@@ -19,7 +18,6 @@
   val is_finished: string -> bool
   val master_directory: string -> Path.T
   val loaded_files: string -> Path.T list
-  val get_parents: string -> string list
   val touch_thy: string -> unit
   val touch_child_thys: string -> unit
   val thy_ord: theory * theory -> order
@@ -44,7 +42,6 @@
 (** theory loader actions and hooks **)
 
 datatype action = Update | Outdate | Remove;
-val str_of_action = fn Update => "Update" | Outdate => "Outdate" | Remove => "Remove";
 
 local
   val hooks = Unsynchronized.ref ([]: (action -> string -> unit) list);