equal
deleted
inserted
replaced
176 if exists (fn (name, _) => name <> "") alt_names |
176 if exists (fn (name, _) => name <> "") alt_names |
177 then writeln "specification" |
177 then writeln "specification" |
178 else () |
178 else () |
179 in |
179 in |
180 arg |
180 arg |
181 |> apsnd Thm.unvarify_global |
181 |> apsnd (Thm.unvarify_global thy) |
182 |> process_all (zip3 alt_names rew_imps frees) |
182 |> process_all (zip3 alt_names rew_imps frees) |
183 end |
183 end |
184 |
184 |
185 fun after_qed [[thm]] = Proof_Context.background_theory (fn thy => |
185 fun after_qed [[thm]] = Proof_Context.background_theory (fn thy => |
186 #1 (post_process (add_specification (zip3 names cnames overloaded) (thy, thm)))); |
186 #1 (post_process (add_specification (zip3 names cnames overloaded) (thy, thm)))); |