# HG changeset patch
# User wenzelm
# Date 963522920 -7200
# Node ID 488e0367a77d8f4ceab4f6d61f3d35b892ad7d92
# Parent  4c3fb078602296724816bcc379128e55fa1d82bc
add_term_consts: ins_string;

diff -r 4c3fb0786022 -r 488e0367a77d src/Pure/term.ML
--- 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;