# HG changeset patch
# User wenzelm
# Date 1319031672 -7200
# Node ID 63ce9e7437347d5d90ec16ee46f60421a9221104
# Parent  d825a8f1d08884b5f109fd8cfda2884aa6933c6b
tuned legacy signature;

diff -r d825a8f1d088 -r 63ce9e743734 src/Tools/misc_legacy.ML
--- a/src/Tools/misc_legacy.ML	Wed Oct 19 14:40:49 2011 +0200
+++ b/src/Tools/misc_legacy.ML	Wed Oct 19 15:41:12 2011 +0200
@@ -5,7 +5,6 @@
 
 signature MISC_LEGACY =
 sig
-  val it_term_types: (typ * 'a -> 'a) -> term * 'a -> 'a
   val add_term_names: term * string list -> string list
   val add_typ_tvars: typ * (indexname * sort) list -> (indexname * sort) list
   val add_typ_tfree_names: typ * string list -> string list