Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
replaced Sign.add_consts_authentic by Sign.declare_const;
authorwenzelm
Thu, 11 Oct 2007 16:05:56 +0200
changeset 24971 4d006b03aa4a
parent 24970 050afeec89a7
child 24972 acafb18a47dc
replaced Sign.add_consts_authentic by Sign.declare_const; tuned;
src/Tools/code/code_package.ML file | annotate | diff | comparison | revisions 
--- 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"
isabelle