add_term_consts: ins_string;
authorwenzelm
Thu Jul 13 23:15:20 2000 +0200 (2000-07-13)
changeset 9319488e0367a77d
parent 9318 4c3fb0786022
child 9320 803cb9c9d4dd
add_term_consts: ins_string;
src/Pure/term.ML
     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;