--- 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;