src/HOL/Tools/BNF/bnf_fp_def_sugar.ML
changeset 55535 10194808430d
parent 55486 8609527278f2
child 55539 0819931d652d
     1.1 --- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Mon Feb 17 13:31:42 2014 +0100
     1.2 +++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Mon Feb 17 13:31:42 2014 +0100
     1.3 @@ -1346,9 +1346,9 @@
     1.4              in
     1.5                (((map_thms, rel_inject_thms, rel_distinct_thms, set_thmss), ctr_sugar),
     1.6                 lthy
     1.7 -               |> Spec_Rules.add Spec_Rules.Equational (`(lhs_heads_of o hd) map_thms)
     1.8 -               |> Spec_Rules.add Spec_Rules.Equational (`(lhs_heads_of o hd) rel_eq_thms)
     1.9 -               |> Spec_Rules.add Spec_Rules.Equational (`(lhs_heads_of o hd) set_thms)
    1.10 +               |> Spec_Rules.add Spec_Rules.Equational (`(single o lhs_head_of o hd) map_thms)
    1.11 +               |> Spec_Rules.add Spec_Rules.Equational (`(single o lhs_head_of o hd) rel_eq_thms)
    1.12 +               |> Spec_Rules.add Spec_Rules.Equational (`(single o lhs_head_of o hd) set_thms)
    1.13                 |> Local_Theory.notes (anonymous_notes @ notes)
    1.14                 |> snd)
    1.15              end;