183 fun process_single ((name,atts),rew_imp,frees) args = |
183 fun process_single ((name,atts),rew_imp,frees) args = |
184 let |
184 let |
185 fun undo_imps thm = |
185 fun undo_imps thm = |
186 Thm.equal_elim (Thm.symmetric rew_imp) thm |
186 Thm.equal_elim (Thm.symmetric rew_imp) thm |
187 |
187 |
188 fun add_final (arg as (thy, thm)) = |
188 fun add_final (thm, thy) = |
189 if name = "" |
189 if name = "" |
190 then arg |> Library.swap |
190 then (thm, thy) |
191 else (writeln (" " ^ name ^ ": " ^ Display.string_of_thm_global thy thm); |
191 else (writeln (" " ^ name ^ ": " ^ Display.string_of_thm_global thy thm); |
192 Global_Theory.store_thm (Binding.name name, thm) thy) |
192 Global_Theory.store_thm (Binding.name name, thm) thy) |
193 in |
193 in |
194 args |> apsnd (remove_alls frees) |
194 swap args |
195 |> apsnd undo_imps |
195 |> apfst (remove_alls frees) |
196 |> apsnd Drule.export_without_context |
196 |> apfst undo_imps |
197 |> Thm.theory_attributes |
197 |> apfst Drule.export_without_context |
|
198 |-> Thm.theory_attributes |
198 (map (Attrib.attribute thy) |
199 (map (Attrib.attribute thy) |
199 (@{attributes [nitpick_choice_spec]} @ atts)) |
200 (@{attributes [nitpick_choice_spec]} @ atts)) |
200 |> add_final |
201 |> add_final |
201 |> Library.swap |
202 |> swap |
202 end |
203 end |
203 |
204 |
204 fun process_all [proc_arg] args = |
205 fun process_all [proc_arg] args = |
205 process_single proc_arg args |
206 process_single proc_arg args |
206 | process_all (proc_arg::rest) (thy,thm) = |
207 | process_all (proc_arg::rest) (thy,thm) = |