removed lookup_const (use Sign.const_type instead); Isabelle94
authorwenzelm
Wed Sep 14 16:11:19 1994 +0200 (1994-09-14)
changeset 613f9eb0f819642
parent 612 1ebe4d36dedc
child 614 da97045ef59a
removed lookup_const (use Sign.const_type instead);
src/Pure/section_utils.ML
     1.1 --- a/src/Pure/section_utils.ML	Wed Sep 14 16:05:39 1994 +0200
     1.2 +++ b/src/Pure/section_utils.ML	Wed Sep 14 16:11:19 1994 +0200
     1.3 @@ -20,8 +20,6 @@
     1.4  
     1.5  fun get_def thy s = get_axiom thy (s^"_def");
     1.6  
     1.7 -fun lookup_const sign a = Symtab.lookup(#const_tab (Sign.rep_sg sign), a);
     1.8 -
     1.9  
    1.10  (*Read an assumption in the given theory*)
    1.11  fun assume_read thy a = assume (read_cterm (sign_of thy) (a,propT));