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 28799 ee65e7d043fc
parent 28496 4cff10648928
child 28814 463c9e9111ae 
--- a/src/Pure/Isar/isar_cmd.ML	Sat Nov 15 21:31:15 2008 +0100
+++ b/src/Pure/Isar/isar_cmd.ML	Sat Nov 15 21:31:17 2008 +0100
@@ -469,7 +469,7 @@
         let
           val (ctxt, (_, thm)) = Proof.get_goal state;
           val thy = ProofContext.theory_of ctxt;
-          val prf = Thm.proof_of thm;
+          val prf = Proofterm.proof_of (Thm.proof_of thm);
           val prop = Thm.full_prop_of thm;
           val prf' = Proofterm.rewrite_proof_notypes ([], []) prf
         in
isabelle