src/HOL/Tools/Datatype/datatype_abs_proofs.ML
changeset 33173 b8ca12f6681a
parent 33171 292970b42770
child 33278 ba9f52f56356
     1.1 --- a/src/HOL/Tools/Datatype/datatype_abs_proofs.ML	Sun Oct 25 20:54:21 2009 +0100
     1.2 +++ b/src/HOL/Tools/Datatype/datatype_abs_proofs.ML	Sun Oct 25 21:35:46 2009 +0100
     1.3 @@ -321,7 +321,7 @@
     1.4                  fns2 @ (flat (Library.drop (i + 1, case_dummy_fns))) )));
     1.5            val ([def_thm], thy') =
     1.6              thy
     1.7 -            |> Sign.declare_const [] decl |> snd
     1.8 +            |> Sign.declare_const decl |> snd
     1.9              |> (PureThy.add_defs false o map Thm.no_attributes) [def];
    1.10  
    1.11          in (defs @ [def_thm], thy')