# HG changeset patch
# User berghofe
# Date 1177420047 -7200
# Node ID 292dbccd875598e9da5fd1ccdbcf1f9f6f779b25
# Parent  d08efe73b27f04fb37886a0230f998e3e89f32c5
case constants are now authentic.

diff -r d08efe73b27f -r 292dbccd8755 src/HOL/Tools/datatype_abs_proofs.ML
--- 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')