changeset 50787 | 065c684130ad |
parent 49444 | fad4724230ce |
child 51658 | 21c10672633b |
--- a/src/HOL/SPARK/Tools/spark_commands.ML Wed Jan 09 20:46:32 2013 +0100 +++ b/src/HOL/SPARK/Tools/spark_commands.ML Tue Jan 08 22:10:02 2013 +0100 @@ -75,7 +75,7 @@ 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 true lthy + (Binding.name vc_name, []) [] ctxt stmt false lthy end; fun string_of_status NONE = "(unproved)"