# HG changeset patch
# User haftmann
# Date 1159196660 -7200
# Node ID f3f2b1091ea0173fb3c50b83e0ad2f4a820b1a75
# Parent  8b79d853eabb7472fd24f69ee15ba5969df0f19f
adding constants the modern way

diff -r 8b79d853eabb -r f3f2b1091ea0 src/Pure/Tools/class_package.ML
--- a/src/Pure/Tools/class_package.ML	Mon Sep 25 17:04:19 2006 +0200
+++ b/src/Pure/Tools/class_package.ML	Mon Sep 25 17:04:20 2006 +0200
@@ -296,7 +296,7 @@
         fun add_global_const ((c, ty), syn) thy =
           ((c, (Sign.full_name thy c, ty)),
             thy
-            |> Sign.add_consts_i [(c, ty |> subst_clsvar v (TFree (v, Sign.defaultS thy)), syn)]);
+            |> Sign.add_consts_authentic [(c, ty |> subst_clsvar v (TFree (v, Sign.defaultS thy)), syn)]);
       in
         thy
         |> fold_map add_global_const raw_cs_this