equal
deleted
inserted
replaced
40 |
40 |
41 fun mk_defname fixes = fixes |> map (fst o fst) |> space_implode "_" |
41 fun mk_defname fixes = fixes |> map (fst o fst) |> space_implode "_" |
42 |
42 |
43 fun add_simps fnames post sort extra_qualify label moreatts simps lthy = |
43 fun add_simps fnames post sort extra_qualify label moreatts simps lthy = |
44 let |
44 let |
45 val atts = Attrib.internal (K Simplifier.simp_add) :: moreatts |
45 val atts = Attrib.internal (K Simplifier.simp_add) :: |
|
46 Attrib.internal (K Nitpick_Const_Simps_Thms.add) :: moreatts |
46 val spec = post simps |
47 val spec = post simps |
47 |> map (apfst (apsnd (append atts))) |
48 |> map (apfst (apsnd (append atts))) |
48 |> map (apfst (apfst extra_qualify)) |
49 |> map (apfst (apfst extra_qualify)) |
49 |
50 |
50 val (saved_spec_simps, lthy) = |
51 val (saved_spec_simps, lthy) = |