# HG changeset patch
# User wenzelm
# Date 779551879 -7200
# Node ID f9eb0f819642b2ad77119dbf8935bf13248f205d
# Parent  1ebe4d36dedc2526d014e75a5eac820230d2ed66
removed lookup_const (use Sign.const_type instead);

diff -r 1ebe4d36dedc -r f9eb0f819642 src/Pure/section_utils.ML
--- a/src/Pure/section_utils.ML	Wed Sep 14 16:05:39 1994 +0200
+++ b/src/Pure/section_utils.ML	Wed Sep 14 16:11:19 1994 +0200
@@ -20,8 +20,6 @@
 
 fun get_def thy s = get_axiom thy (s^"_def");
 
-fun lookup_const sign a = Symtab.lookup(#const_tab (Sign.rep_sg sign), a);
-
 
 (*Read an assumption in the given theory*)
 fun assume_read thy a = assume (read_cterm (sign_of thy) (a,propT));