Sign.add_const_constraint;
authorwenzelm
Sat Sep 29 21:39:45 2007 +0200 (2007-09-29 ago)
changeset 247603f9aa1e13d16
parent 24759 b448f94b1c88
child 24761 d762ab297a07
Sign.add_const_constraint;
src/Pure/axclass.ML
     1.1 --- a/src/Pure/axclass.ML	Sat Sep 29 21:39:44 2007 +0200
     1.2 +++ b/src/Pure/axclass.ML	Sat Sep 29 21:39:45 2007 +0200
     1.3 @@ -378,7 +378,7 @@
     1.4        |> (map o apsnd o map) (Sign.cert_prop thy)
     1.5        |> rpair thy;
     1.6      fun add_constraint class (c, ty) =
     1.7 -      Sign.add_const_constraint_i (c, SOME
     1.8 +      Sign.add_const_constraint (c, SOME
     1.9          (Term.map_type_tfree (fn (v, _) => TFree (v, [class])) ty));
    1.10    in
    1.11      thy