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/calculation.ML
changeset 63541 e308f15cc8a7
parent 63368 e9e677b73011
child 63543 e6e057c01401 
--- a/src/Pure/Isar/calculation.ML	Fri Jul 22 11:00:43 2016 +0200
+++ b/src/Pure/Isar/calculation.ML	Fri Jul 22 11:01:10 2016 +0200
@@ -122,7 +122,9 @@
 
 fun maintain_calculation int final calc state =
   let
-    val state' = put_calculation (SOME calc) state;
+    val state' = state
+      |> put_calculation (SOME calc)
+      |> Proof.improper_reset_facts;
     val ctxt' = Proof.context_of state';
     val _ =
       if int then
isabelle