# HG changeset patch
# User wenzelm
# Date 1191094785 -7200
# Node ID 3f9aa1e13d164dd509e8c0b0cb4d76b67bf84c81
# Parent  b448f94b1c882ab6f704b56ad03654e4f5e8f8b5
Sign.add_const_constraint;

diff -r b448f94b1c88 -r 3f9aa1e13d16 src/Pure/axclass.ML
--- a/src/Pure/axclass.ML	Sat Sep 29 21:39:44 2007 +0200
+++ b/src/Pure/axclass.ML	Sat Sep 29 21:39:45 2007 +0200
@@ -378,7 +378,7 @@
       |> (map o apsnd o map) (Sign.cert_prop thy)
       |> rpair thy;
     fun add_constraint class (c, ty) =
-      Sign.add_const_constraint_i (c, SOME
+      Sign.add_const_constraint (c, SOME
         (Term.map_type_tfree (fn (v, _) => TFree (v, [class])) ty));
   in
     thy