Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/Pure/Isar/isar_cmd.ML
changeset 26626 c6231d64d264
parent 26599 791e4b436f8a
child 26671 c95590e01df5 
--- a/src/Pure/Isar/isar_cmd.ML	Thu Apr 10 20:54:18 2008 +0200
+++ b/src/Pure/Isar/isar_cmd.ML	Sat Apr 12 17:00:35 2008 +0200
@@ -564,7 +564,8 @@
       NONE =>
         let
           val (ctxt, (_, thm)) = Proof.get_goal state;
-          val {thy, der = (_, prf), ...} = Thm.rep_thm thm;
+          val thy = ProofContext.theory_of ctxt;
+          val prf = Thm.proof_of thm;
           val prop = Thm.full_prop_of thm;
           val prf' = Proofterm.rewrite_proof_notypes ([], []) prf
         in
isabelle