equal
deleted
inserted
replaced
136 |
136 |
137 local |
137 local |
138 |
138 |
139 fun apply change_naming (interp: interp) (data: data) lthy = |
139 fun apply change_naming (interp: interp) (data: data) lthy = |
140 lthy |
140 lthy |
141 |> change_naming ? Local_Theory.map_naming (K (#naming data)) |
141 |> change_naming ? Local_Theory.map_background_naming (K (#naming data)) |
142 |> #apply interp (#value data) |
142 |> #apply interp (#value data) |
143 |> Local_Theory.restore_naming lthy; |
143 |> Local_Theory.restore_background_naming lthy; |
144 |
144 |
145 fun unfinished data (interp: interp, data') = |
145 fun unfinished data (interp: interp, data') = |
146 (interp, |
146 (interp, |
147 if eq_list eq_data (data, data') then [] |
147 if eq_list eq_data (data, data') then [] |
148 else data |> filter (fn d => #filter d (#name interp) andalso not (member eq_data data' d))); |
148 else data |> filter (fn d => #filter d (#name interp) andalso not (member eq_data data' d))); |