adding code equations for constructors
authorhaftmann
Wed Nov 11 15:10:26 2009 +0100 (2009-11-11)
changeset 336122640cc1cfc2e
parent 33611 168b928d5024
child 33613 ad27f52ee759
adding code equations for constructors
src/HOL/Tools/record.ML
     1.1 --- a/src/HOL/Tools/record.ML	Wed Nov 11 10:06:30 2009 +0100
     1.2 +++ b/src/HOL/Tools/record.ML	Wed Nov 11 15:10:26 2009 +0100
     1.3 @@ -1754,11 +1754,12 @@
     1.4  
     1.5      val ([inject', induct', surjective', split_meta'], thm_thy) =
     1.6        defs_thy
     1.7 -      |> (PureThy.add_thms o map (Thm.no_attributes o apfst Binding.name))
     1.8 +      |> PureThy.add_thms (map (Thm.no_attributes o apfst Binding.name)
     1.9             [("ext_inject", inject),
    1.10              ("ext_induct", induct),
    1.11              ("ext_surjective", surject),
    1.12 -            ("ext_split", split_meta)];
    1.13 +            ("ext_split", split_meta)])
    1.14 +      ||> Code.add_default_eqn ext_def;
    1.15  
    1.16    in (thm_thy, extT, induct', inject', split_meta', ext_def) end;
    1.17