Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Tools/datatype_abs_proofs.ML
changeset 22776 292dbccd8755
parent 22578 b0eb5652f210
child 22994 02440636214f 
--- 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