equal
deleted
inserted
replaced
165 in fn ty => fn s => proof_of_term thy ty (Logic.varify_global (rd s)) end; |
165 in fn ty => fn s => proof_of_term thy ty (Logic.varify_global (rd s)) end; |
166 |
166 |
167 fun proof_syntax prf = |
167 fun proof_syntax prf = |
168 let |
168 let |
169 val thm_names = Symtab.keys (Proofterm.fold_proof_atoms true |
169 val thm_names = Symtab.keys (Proofterm.fold_proof_atoms true |
170 (fn PThm (_, ((name, _, _), _)) => if name <> "" then Symtab.update (name, ()) else I |
170 (fn PThm (_, ((name, _, _, _), _)) => if name <> "" then Symtab.update (name, ()) else I |
171 | _ => I) [prf] Symtab.empty); |
171 | _ => I) [prf] Symtab.empty); |
172 val axm_names = Symtab.keys (Proofterm.fold_proof_atoms true |
172 val axm_names = Symtab.keys (Proofterm.fold_proof_atoms true |
173 (fn PAxm (name, _, _) => Symtab.update (name, ()) | _ => I) [prf] Symtab.empty); |
173 (fn PAxm (name, _, _) => Symtab.update (name, ()) | _ => I) [prf] Symtab.empty); |
174 in |
174 in |
175 add_proof_syntax #> |
175 add_proof_syntax #> |
182 val thm = Thm.transfer' ctxt raw_thm; |
182 val thm = Thm.transfer' ctxt raw_thm; |
183 val prop = Thm.full_prop_of thm; |
183 val prop = Thm.full_prop_of thm; |
184 val prf = Thm.proof_of thm; |
184 val prf = Thm.proof_of thm; |
185 val prf' = |
185 val prf' = |
186 (case Proofterm.strip_combt (fst (Proofterm.strip_combP prf)) of |
186 (case Proofterm.strip_combt (fst (Proofterm.strip_combP prf)) of |
187 (PThm (_, ((_, prop', _), body)), _) => |
187 (PThm (_, ((_, prop', _, _), body)), _) => |
188 if prop = prop' then Proofterm.join_proof body else prf |
188 if prop = prop' then Proofterm.join_proof body else prf |
189 | _ => prf) |
189 | _ => prf) |
190 in if full then Reconstruct.reconstruct_proof ctxt prop prf' else prf' end; |
190 in if full then Reconstruct.reconstruct_proof ctxt prop prf' else prf' end; |
191 |
191 |
192 fun pretty_proof ctxt prf = |
192 fun pretty_proof ctxt prf = |