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.
case constants are now authentic.
authorberghofe
Tue, 24 Apr 2007 15:07:27 +0200
changeset 22776 292dbccd8755
parent 22775 d08efe73b27f
child 22777 2fc921376a86
case constants are now authentic.
src/HOL/Tools/datatype_abs_proofs.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/Tools/datatype_abs_proofs.ML	Tue Apr 24 14:02:16 2007 +0200
+++ b/src/HOL/Tools/datatype_abs_proofs.ML	Tue Apr 24 15:07:27 2007 +0200
@@ -324,7 +324,7 @@
                 fns2 @ (List.concat (Library.drop (i + 1, case_dummy_fns))) )));
           val ([def_thm], thy') =
             thy
-            |> Theory.add_consts_i [decl]
+            |> Sign.add_consts_authentic [decl]
             |> (PureThy.add_defs_i false o map Thm.no_attributes) [def];
 
         in (defs @ [def_thm], thy')
isabelle