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/HOL/Boogie/Tools/boogie_commands.ML
changeset 33445 f0c78a28e18e
parent 33419 8ae45e87b992
child 33671 4b0f2599ed48 
--- a/src/HOL/Boogie/Tools/boogie_commands.ML	Thu Nov 05 14:41:37 2009 +0100
+++ b/src/HOL/Boogie/Tools/boogie_commands.ML	Thu Nov 05 14:48:40 2009 +0100
@@ -40,7 +40,11 @@
         fun store thm = Boogie_VCs.discharge (name, thm)
         fun after_qed [[thm]] = LocalTheory.theory (store thm)
           | after_qed _ = I
-      in lthy |> Proof.theorem_i NONE after_qed [[(vc, [])]] end)
+      in
+        lthy
+        |> Variable.auto_fixes vc
+        |> Proof.theorem_i NONE after_qed [[(vc, [])]]
+      end)
 
 fun boogie_end thy =
   let
isabelle