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/goal.ML
changeset 60723 757cad5a3fe9
parent 60722 a8babbb6d5ea
child 60819 e1f1842bf344 
--- a/src/Pure/goal.ML	Tue Jul 14 11:29:43 2015 +0200
+++ b/src/Pure/goal.ML	Tue Jul 14 19:01:46 2015 +0200
@@ -231,7 +231,7 @@
           (Thm.term_of stmt);
   in
     res
-    |> length props > 1 ? Thm.norm_proof
+    |> length props > 1 ? Thm.close_derivation
     |> Conjunction.elim_balanced (length props)
     |> map (Assumption.export false ctxt' ctxt)
     |> Variable.export ctxt' ctxt
isabelle