src/ZF/ind_syntax.ML

--- a/src/ZF/ind_syntax.ML	Fri Sep 17 12:53:53 1993 +0200
+++ b/src/ZF/ind_syntax.ML	Fri Sep 17 16:16:38 1993 +0200
@@ -37,7 +37,6 @@
        flatten_term sign (Logic.mk_equals (lhs,rhs)))
   end;
 
-(*export to Pure/sign?  Used in Provers/simp.ML...*)
 fun lookup_const sign a = Symtab.lookup(#const_tab (Sign.rep_sg sign), a);
 
 (*export to Pure/library?  *)