src/Pure/term.ML
changeset 9319 488e0367a77d
parent 8609 ec57bc9340e8
child 9536 b79b002f32ae
     1.1 --- a/src/Pure/term.ML	Thu Jul 13 23:14:49 2000 +0200
     1.2 +++ b/src/Pure/term.ML	Thu Jul 13 23:15:20 2000 +0200
     1.3 @@ -746,7 +746,7 @@
     1.4  val add_term_classes = it_term_types add_typ_classes;
     1.5  val add_term_tycons = it_term_types add_typ_tycons;
     1.6  
     1.7 -fun add_term_consts (Const (c, _), cs) = c ins cs
     1.8 +fun add_term_consts (Const (c, _), cs) = c ins_string cs
     1.9    | add_term_consts (t $ u, cs) = add_term_consts (t, add_term_consts (u, cs))
    1.10    | add_term_consts (Abs (_, _, t), cs) = add_term_consts (t, cs)
    1.11    | add_term_consts (_, cs) = cs;