# HG changeset patch
# User wenzelm
# Date 1463226721 -7200
# Node ID 3081f7719df741f8e1f48a8f5fb5c1a39612c831
# Parent  a949b2a5f51d01bebe1d00d2144f7dfc17d5cd1b
reverted accidental commit;

diff -r a949b2a5f51d -r 3081f7719df7 src/HOL/SPARK/Tools/spark_commands.ML
--- a/src/HOL/SPARK/Tools/spark_commands.ML	Fri May 13 20:24:10 2016 +0200
+++ b/src/HOL/SPARK/Tools/spark_commands.ML	Sat May 14 13:52:01 2016 +0200
@@ -48,7 +48,7 @@
     val thy = Proof_Context.theory_of lthy;
     val (ctxt, stmt) = get_vc thy vc_name
   in
-    Specification.theorem true Thm.theoremK NONE
+    Specification.theorem Thm.theoremK NONE
       (fn thmss => (Local_Theory.background_theory
          (SPARK_VCs.mark_proved vc_name (flat thmss))))
       (Binding.name vc_name, []) [] ctxt stmt false lthy