equal
deleted
inserted
replaced
56 |> map (apfst (apfst extra_qualify)) |
56 |> map (apfst (apfst extra_qualify)) |
57 |
57 |
58 val (saved_spec_simps, lthy) = |
58 val (saved_spec_simps, lthy) = |
59 fold_map (LocalTheory.note Thm.generatedK) spec lthy |
59 fold_map (LocalTheory.note Thm.generatedK) spec lthy |
60 |
60 |
61 val saved_simps = flat (map snd saved_spec_simps) |
61 val saved_simps = maps snd saved_spec_simps |
62 val simps_by_f = sort saved_simps |
62 val simps_by_f = sort saved_simps |
63 |
63 |
64 fun add_for_f fname simps = |
64 fun add_for_f fname simps = |
65 note_theorem ((Long_Name.qualify fname label, []), simps) #> snd |
65 note_theorem ((Long_Name.qualify fname label, []), simps) #> snd |
66 in |
66 in |