src/HOL/SPARK/Tools/spark_commands.ML
changeset 63093 3081f7719df7
parent 63092 a949b2a5f51d
child 63094 056ea294c256
equal deleted inserted replaced
63092:a949b2a5f51d 63093:3081f7719df7
    46 fun prove_vc vc_name lthy =
    46 fun prove_vc vc_name lthy =
    47   let
    47   let
    48     val thy = Proof_Context.theory_of lthy;
    48     val thy = Proof_Context.theory_of lthy;
    49     val (ctxt, stmt) = get_vc thy vc_name
    49     val (ctxt, stmt) = get_vc thy vc_name
    50   in
    50   in
    51     Specification.theorem true Thm.theoremK NONE
    51     Specification.theorem Thm.theoremK NONE
    52       (fn thmss => (Local_Theory.background_theory
    52       (fn thmss => (Local_Theory.background_theory
    53          (SPARK_VCs.mark_proved vc_name (flat thmss))))
    53          (SPARK_VCs.mark_proved vc_name (flat thmss))))
    54       (Binding.name vc_name, []) [] ctxt stmt false lthy
    54       (Binding.name vc_name, []) [] ctxt stmt false lthy
    55   end;
    55   end;
    56 
    56