removed lookup_const (use Sign.const_type instead); Isabelle94
authorwenzelm
Wed, 14 Sep 1994 16:11:19 +0200
changeset 613 f9eb0f819642
parent 612 1ebe4d36dedc
child 614 da97045ef59a
removed lookup_const (use Sign.const_type instead);
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));