summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

src/Pure/Proof/proof_syntax.ML

changeset 13530 | 4813fdc0ef17 |

parent 13199 | 18402c1f76bf |

child 14854 | 61bdf2ae4dc5 |

1.1 --- a/src/Pure/Proof/proof_syntax.ML Tue Aug 27 11:06:07 2002 +0200 1.2 +++ b/src/Pure/Proof/proof_syntax.ML Tue Aug 27 11:06:20 2002 +0200 1.3 @@ -147,7 +147,7 @@ 1.4 | "thm" :: xs => 1.5 let val name = NameSpace.pack xs; 1.6 in (case assoc (thms, name) of 1.7 - Some thm => fst (strip_combt (#2 (#der (rep_thm thm)))) 1.8 + Some thm => fst (strip_combt (Thm.proof_of thm)) 1.9 | None => (case Symtab.lookup (tab, name) of 1.10 Some prf => prf 1.11 | None => error ("Unknown theorem " ^ quote name)))