# HG changeset patch
# User wenzelm
# Date 1192111556 -7200
# Node ID 4d006b03aa4aca828132e0f226d1bfcfd725560f
# Parent  050afeec89a73752ee47796ada3fb2ba64c73327
replaced Sign.add_consts_authentic by Sign.declare_const;
tuned;

diff -r 050afeec89a7 -r 4d006b03aa4a src/Tools/code/code_package.ML
--- a/src/Tools/code/code_package.ML	Thu Oct 11 16:05:53 2007 +0200
+++ b/src/Tools/code/code_package.ML	Thu Oct 11 16:05:56 2007 +0200
@@ -199,11 +199,10 @@
         val _ = warning ("Adding theorem " ^ quote (PureThy.string_of_thmref thmref)
           ^ " as code property " ^ quote raw_c);
         val ([raw_c'], names') = Name.variants [raw_c] names;
-      in
-        thy
-        |> PureThy.simple_def ("", []) (((raw_c', ty, Syntax.NoSyn), ts), t)
-        ||> pair names'
-      end;
+        val (const as Const (c, _), thy') = thy |> Sign.declare_const [] (raw_c', ty, NoSyn);
+        val eq = Logic.mk_equals (list_comb (const, ts), t);
+        val ([def], thy'') = thy' |> PureThy.add_defs_i false [((Thm.def_name raw_c', eq), [])];
+      in ((c, def), (names', thy'')) end;
   in
     thy
     |> Sign.sticky_prefix "codeprop"