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 24770 695a8e087b9f
parent 24746 6d42be359d57
child 24814 0384f48a806e 
--- a/src/HOL/Tools/datatype_abs_proofs.ML	Sun Sep 30 11:55:14 2007 +0200
+++ b/src/HOL/Tools/datatype_abs_proofs.ML	Sun Sep 30 16:20:31 2007 +0200
@@ -320,7 +320,7 @@
                 fns2 @ (List.concat (Library.drop (i + 1, case_dummy_fns))) )));
           val ([def_thm], thy') =
             thy
-            |> Sign.add_consts_authentic [decl]
+            |> Sign.add_consts_authentic [] [decl]
             |> (PureThy.add_defs_i false o map Thm.no_attributes) [def];
 
         in (defs @ [def_thm], thy')
isabelle