reverted accidental commit;
authorwenzelm
Sat May 14 13:52:01 2016 +0200 (2016-05-14 ago)
changeset 630933081f7719df7
parent 63092 a949b2a5f51d
child 63094 056ea294c256
reverted accidental commit;
src/HOL/SPARK/Tools/spark_commands.ML
     1.1 --- a/src/HOL/SPARK/Tools/spark_commands.ML	Fri May 13 20:24:10 2016 +0200
     1.2 +++ b/src/HOL/SPARK/Tools/spark_commands.ML	Sat May 14 13:52:01 2016 +0200
     1.3 @@ -48,7 +48,7 @@
     1.4      val thy = Proof_Context.theory_of lthy;
     1.5      val (ctxt, stmt) = get_vc thy vc_name
     1.6    in
     1.7 -    Specification.theorem true Thm.theoremK NONE
     1.8 +    Specification.theorem Thm.theoremK NONE
     1.9        (fn thmss => (Local_Theory.background_theory
    1.10           (SPARK_VCs.mark_proved vc_name (flat thmss))))
    1.11        (Binding.name vc_name, []) [] ctxt stmt false lthy