1.1 --- a/src/HOL/SPARK/Tools/spark_vcs.ML	Fri Mar 04 11:43:20 2011 +0100
     1.2 +++ b/src/HOL/SPARK/Tools/spark_vcs.ML	Fri Mar 04 17:39:30 2011 +0100
     1.3 @@ -13,11 +13,11 @@
     1.4      string * ((string list * string) option * 'a) ->
     1.5      theory -> theory
     1.6    val lookup_vc: theory -> string -> (Element.context_i list *
     1.7 -    (string * bool * Element.context_i * Element.statement_i)) option
     1.8 +    (string * thm list option * Element.context_i * Element.statement_i)) option
     1.9    val get_vcs: theory ->
    1.10 -    Element.context_i list * (binding * thm) list *
    1.11 -    (string * (string * bool * Element.context_i * Element.statement_i)) list
    1.12 -  val mark_proved: string -> theory -> theory
    1.13 +    Element.context_i list * (binding * thm) list * (string *
    1.14 +    (string * thm list option * Element.context_i * Element.statement_i)) list
    1.15 +  val mark_proved: string -> thm list -> theory -> theory
    1.16    val close: theory -> theory
    1.17    val is_closed: theory -> bool
    1.18  end;
    1.19 @@ -616,7 +616,7 @@
    1.20          funs: (string list * string) tab,
    1.21          ids: (term * string) Symtab.table * Name.context,
    1.22          proving: bool,
    1.23 -        vcs: (string * bool *
    1.24 +        vcs: (string * thm list option *
    1.25            (string * expr) list * (string * expr) list) VCtab.table,
    1.26          path: Path.T} option}
    1.27    val empty : T = {pfuns = Symtab.empty, env = NONE}
    1.28 @@ -713,27 +713,28 @@
    1.29        end
    1.30    | _ => ([], [], []));
    1.31  
    1.32 -fun mark_proved name = VCs.map (fn
    1.33 +fun mark_proved name thms = VCs.map (fn
    1.34      {pfuns, env = SOME {ctxt, defs, types, funs, ids, vcs, path, ...}} =>
    1.35        {pfuns = pfuns,
    1.36         env = SOME {ctxt = ctxt, defs = defs,
    1.37           types = types, funs = funs, ids = ids,
    1.38           proving = true,
    1.39           vcs = VCtab.map_entry name (fn (trace, _, ps, cs) =>
    1.40 -           (trace, true, ps, cs)) vcs,
    1.41 +           (trace, SOME thms, ps, cs)) vcs,
    1.42           path = path}}
    1.43    | x => x);
    1.44  
    1.45  fun close thy = VCs.map (fn
    1.46      {pfuns, env = SOME {vcs, path, ...}} =>
    1.47 -      (case VCtab.fold_rev (fn (s, (_, p, _, _)) =>
    1.48 -           (if p then apfst else apsnd) (cons s)) vcs ([], []) of
    1.49 +      (case VCtab.fold_rev (fn vc as (_, (_, p, _, _)) =>
    1.50 +           (if is_some p then apfst else apsnd) (cons vc)) vcs ([], []) of
    1.51           (proved, []) =>
    1.52 -           (File.write (Path.ext "prv" path)
    1.53 -              (concat (map (fn s => snd (strip_number s) ^
    1.54 +           (Thm.join_proofs (maps (the o #2 o snd) proved);
    1.55 +            File.write (Path.ext "prv" path)
    1.56 +              (concat (map (fn (s, _) => snd (strip_number s) ^
    1.57                   " -- proved by " ^ Distribution.version ^ "\n") proved));
    1.58              {pfuns = pfuns, env = NONE})
    1.59 -       | (_, unproved) => err_vcs unproved)
    1.60 +       | (_, unproved) => err_vcs (map fst unproved))
    1.61    | x => x) thy;
    1.62  
    1.63  
    1.64 @@ -834,7 +835,7 @@
    1.65        else warning ("Ignoring rules: " ^ rulenames rules'');
    1.66  
    1.67      val vcs' = VCtab.make (maps (fn (tr, vcs) =>
    1.68 -      map (fn (s, (ps, cs)) => (s, (tr, false, ps, cs)))
    1.69 +      map (fn (s, (ps, cs)) => (s, (tr, NONE, ps, cs)))
    1.70          (filter_out (is_trivial_vc o snd) vcs)) vcs);
    1.71  
    1.72      val _ = (case filter_out (is_some o lookup funs)