author | wenzelm |
Sat, 14 May 2016 13:52:01 +0200 | |
changeset 63093 | 3081f7719df7 |
parent 63092 | a949b2a5f51d |
child 63094 | 056ea294c256 |
--- 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