add_term_consts: ins_string;

--- a/src/Pure/term.ML	Thu Jul 13 23:14:49 2000 +0200
+++ b/src/Pure/term.ML	Thu Jul 13 23:15:20 2000 +0200
@@ -746,7 +746,7 @@
 val add_term_classes = it_term_types add_typ_classes;
 val add_term_tycons = it_term_types add_typ_tycons;
 
-fun add_term_consts (Const (c, _), cs) = c ins cs
+fun add_term_consts (Const (c, _), cs) = c ins_string cs
   | add_term_consts (t $ u, cs) = add_term_consts (t, add_term_consts (u, cs))
   | add_term_consts (Abs (_, _, t), cs) = add_term_consts (t, cs)
   | add_term_consts (_, cs) = cs;