merged
authorwenzelm
Fri Dec 16 19:50:46 2016 +0100 (2016-12-16)
changeset 64575d44f0b714e13
parent 64561 a7664ca9ffc5
parent 64574 1134e4d5e5b7
child 64576 ce8802dc3145
merged
     1.1 --- a/src/HOL/Library/Old_SMT/old_z3_proof_reconstruction.ML	Thu Dec 15 15:05:35 2016 +0100
     1.2 +++ b/src/HOL/Library/Old_SMT/old_z3_proof_reconstruction.ML	Fri Dec 16 19:50:46 2016 +0100
     1.3 @@ -167,7 +167,7 @@
     1.4        assms
     1.5        |> map (apsnd (rewrite ctxt eqs'))
     1.6        |> map (apsnd (Conv.fconv_rule Thm.eta_conversion))
     1.7 -      |> Old_Z3_Proof_Tools.thm_net_of snd 
     1.8 +      |> Old_Z3_Proof_Tools.thm_net_of snd
     1.9  
    1.10      fun revert_conv ctxt = rewrite_conv ctxt eqs' then_conv Thm.eta_conversion
    1.11  
    1.12 @@ -183,14 +183,14 @@
    1.13            if exact then (Thm.implies_elim thm1 th, ctxt)
    1.14            else assume thm1 ctxt
    1.15          val thms' = if exact then thms else th :: thms
    1.16 -      in 
    1.17 +      in
    1.18          ((insert (op =) i is, thms'),
    1.19            (ctxt', Inttab.update (idx, Thm thm) ptab))
    1.20        end
    1.21  
    1.22      fun add (idx, ct) (cx as ((is, thms), (ctxt, ptab))) =
    1.23        let
    1.24 -        val thm1 = 
    1.25 +        val thm1 =
    1.26            Thm.trivial ct
    1.27            |> Conv.fconv_rule (Conv.arg1_conv (revert_conv outer_ctxt))
    1.28          val thm2 = singleton (Variable.export ctxt outer_ctxt) thm1
    1.29 @@ -218,7 +218,7 @@
    1.30    val mp_c = precomp (Thm.dest_binop o Thm.dest_arg) @{thm mp}
    1.31  in
    1.32  fun mp (MetaEq thm) p = Thm (Thm.implies_elim (comp meta_iffD1_c thm) p)
    1.33 -  | mp p_q p = 
    1.34 +  | mp p_q p =
    1.35        let
    1.36          val pq = thm_of p_q
    1.37          val thm = comp iffD1_c pq handle THM _ => comp mp_c pq
    1.38 @@ -509,7 +509,7 @@
    1.39      (case lookup (Logic.mk_equals (apply2 Thm.term_of cp)) of
    1.40        SOME eq => eq
    1.41      | NONE => if exn then raise MONO else prove_refl cp)
    1.42 -  
    1.43 +
    1.44    val prove_exn = prove_eq true
    1.45    and prove_safe = prove_eq false
    1.46  
    1.47 @@ -752,7 +752,9 @@
    1.48  fun check_after idx r ps ct (p, (ctxt, _)) =
    1.49    if not (Config.get ctxt Old_SMT_Config.trace) then ()
    1.50    else
    1.51 -    let val thm = thm_of p |> tap (Thm.join_proofs o single)
    1.52 +    let
    1.53 +      val thm = thm_of p
    1.54 +      val _ = Thm.consolidate thm
    1.55      in
    1.56        if (Thm.cprop_of thm) aconvc ct then ()
    1.57        else
    1.58 @@ -852,7 +854,7 @@
    1.59  
    1.60    fun discharge_assms_tac ctxt rules =
    1.61      REPEAT (HEADGOAL (resolve_tac ctxt rules ORELSE' SOLVED' (discharge_sk_tac ctxt)))
    1.62 -    
    1.63 +
    1.64    fun discharge_assms ctxt rules thm =
    1.65      if Thm.nprems_of thm = 0 then Goal.norm_result ctxt thm
    1.66      else
    1.67 @@ -881,7 +883,7 @@
    1.68      if Config.get ctxt2 Old_SMT_Config.filter_only_facts then (is, @{thm TrueI})
    1.69      else
    1.70        (Thm @{thm TrueI}, cxp)
    1.71 -      |> fold (prove simpset vars) steps 
    1.72 +      |> fold (prove simpset vars) steps
    1.73        |> discharge rules outer_ctxt
    1.74        |> pair []
    1.75    end
     2.1 --- a/src/HOL/Mirabelle/Tools/mirabelle.ML	Thu Dec 15 15:05:35 2016 +0100
     2.2 +++ b/src/HOL/Mirabelle/Tools/mirabelle.ML	Fri Dec 16 19:50:46 2016 +0100
     2.3 @@ -165,15 +165,17 @@
     2.4  
     2.5  fun fold_body_thms f =
     2.6    let
     2.7 -    fun app n (PBody {thms, ...}) = thms |> fold (fn (i, (name, prop, body)) =>
     2.8 +    fun app n (PBody {thms, ...}) = thms |> fold (fn (i, thm_node) =>
     2.9        fn (x, seen) =>
    2.10          if Inttab.defined seen i then (x, seen)
    2.11          else
    2.12            let
    2.13 -            val body' = Future.join body
    2.14 -            val (x', seen') = app (n + (if name = "" then 0 else 1)) body'
    2.15 +            val name = Proofterm.thm_node_name thm_node
    2.16 +            val prop = Proofterm.thm_node_prop thm_node
    2.17 +            val body = Future.join (Proofterm.thm_node_body thm_node)
    2.18 +            val (x', seen') = app (n + (if name = "" then 0 else 1)) body
    2.19                (x, Inttab.update (i, ()) seen)
    2.20 -        in (x' |> n = 0 ? f (name, prop, body'), seen') end)
    2.21 +        in (x' |> n = 0 ? f (name, prop, body), seen') end)
    2.22    in fn bodies => fn x => #1 (fold (app 0) bodies (x, Inttab.empty)) end
    2.23  
    2.24  in
     3.1 --- a/src/HOL/Proofs/ex/Proof_Terms.thy	Thu Dec 15 15:05:35 2016 +0100
     3.2 +++ b/src/HOL/Proofs/ex/Proof_Terms.thy	Fri Dec 16 19:50:46 2016 +0100
     3.3 @@ -30,7 +30,7 @@
     3.4    (*all theorems used in the graph of nested proofs*)
     3.5    val all_thms =
     3.6      Proofterm.fold_body_thms
     3.7 -      (fn (name, _, _) => insert (op =) name) [body] [];
     3.8 +      (fn {name, ...} => insert (op =) name) [body] [];
     3.9  \<close>
    3.10  
    3.11  text \<open>
     4.1 --- a/src/HOL/ROOT	Thu Dec 15 15:05:35 2016 +0100
     4.2 +++ b/src/HOL/ROOT	Fri Dec 16 19:50:46 2016 +0100
     4.3 @@ -18,10 +18,9 @@
     4.4    description {*
     4.5      HOL-Main with explicit proof terms.
     4.6    *}
     4.7 -  options [document = false, quick_and_dirty = false]
     4.8 +  options [document = false, quick_and_dirty = false, parallel_proofs = 0]
     4.9    theories Proofs (*sequential change of global flag!*)
    4.10 -  theories List
    4.11 -  theories [checkpoint] "~~/src/HOL/Library/Old_Datatype"
    4.12 +  theories "~~/src/HOL/Library/Old_Datatype"
    4.13    files
    4.14      "Tools/Quickcheck/Narrowing_Engine.hs"
    4.15      "Tools/Quickcheck/PNF_Narrowing_Engine.hs"
     5.1 --- a/src/HOL/SPARK/Tools/spark_vcs.ML	Thu Dec 15 15:05:35 2016 +0100
     5.2 +++ b/src/HOL/SPARK/Tools/spark_vcs.ML	Fri Dec 16 19:50:46 2016 +0100
     5.3 @@ -293,7 +293,7 @@
     5.4    | SOME _ => error ("Cannot associate a type with " ^ s ^
     5.5        "\nsince it is no record or enumeration type");
     5.6  
     5.7 -fun check_enum [] [] = NONE 
     5.8 +fun check_enum [] [] = NONE
     5.9    | check_enum els [] = SOME ("has no element(s) " ^ commas els)
    5.10    | check_enum [] cs = SOME ("has extra element(s) " ^
    5.11        commas (map (Long_Name.base_name o fst) cs))
    5.12 @@ -305,7 +305,7 @@
    5.13  fun invert_map [] = I
    5.14    | invert_map cmap =
    5.15        map (apfst (the o AList.lookup (op =) (map swap cmap)));
    5.16 - 
    5.17 +
    5.18  fun add_type_def prfx (s, Basic_Type ty) (ids, thy) =
    5.19        (check_no_assoc thy prfx s;
    5.20         (ids,
    5.21 @@ -677,7 +677,7 @@
    5.22     "+", "-", "*", "/", "div", "mod", "**"]);
    5.23  
    5.24  fun complex_expr (Number _) = false
    5.25 -  | complex_expr (Ident _) = false 
    5.26 +  | complex_expr (Ident _) = false
    5.27    | complex_expr (Funct (s, es)) =
    5.28        not (Symtab.defined builtin s) orelse exists complex_expr es
    5.29    | complex_expr (Quantifier (_, _, _, e)) = complex_expr e
    5.30 @@ -959,7 +959,7 @@
    5.31      | SOME {vcs, path, ...} =>
    5.32          let
    5.33            val (proved, unproved) = partition_vcs vcs;
    5.34 -          val _ = Thm.join_proofs (maps (#2 o snd) proved);
    5.35 +          val _ = List.app Thm.consolidate (maps (#2 o snd) proved);
    5.36            val (proved', proved'') =
    5.37              List.partition (fn (_, (_, thms, _, _)) =>
    5.38                exists (#oracle o Thm.peek_status) thms) proved;
    5.39 @@ -1117,7 +1117,7 @@
    5.40            [(term_of_rule thy' prfx types pfuns ids rl, [])]))
    5.41             other_rules),
    5.42         Element.Notes ("", [((Binding.name "defns", []), map (rpair [] o single o snd) defs')])]
    5.43 -          
    5.44 +
    5.45    in
    5.46      set_env ctxt defs' types funs ids vcs' path prfx thy'
    5.47    end;
     6.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML	Thu Dec 15 15:05:35 2016 +0100
     6.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML	Fri Dec 16 19:50:46 2016 +0100
     6.3 @@ -84,8 +84,10 @@
     6.4     be missing over there; or maybe the two code portions are not doing the same? *)
     6.5  fun fold_body_thm max_thms outer_name (map_plain_name, map_inclass_name) body =
     6.6    let
     6.7 -    fun app_thm map_name (_, (name, _, body)) (accum as (num_thms, names)) =
     6.8 +    fun app_thm map_name (_, thm_node) (accum as (num_thms, names)) =
     6.9        let
    6.10 +        val name = Proofterm.thm_node_name thm_node
    6.11 +        val body = Proofterm.thm_node_body thm_node
    6.12          val (anonymous, enter_class) =
    6.13            (* The "name = outer_name" case caters for the uncommon case where the proved theorem
    6.14               occurs in its own proof (e.g., "Transitive_Closure.trancl_into_trancl"). *)
     7.1 --- a/src/Pure/Concurrent/multithreading.ML	Thu Dec 15 15:05:35 2016 +0100
     7.2 +++ b/src/Pure/Concurrent/multithreading.ML	Fri Dec 16 19:50:46 2016 +0100
     7.3 @@ -61,7 +61,7 @@
     7.4  val trace = ref 0;
     7.5  
     7.6  fun tracing level msg =
     7.7 -  if level > ! trace then ()
     7.8 +  if ! trace < level then ()
     7.9    else Thread_Attributes.uninterruptible (fn _ => fn () =>
    7.10      (TextIO.output (TextIO.stdErr, (">>> " ^ msg () ^ "\n")); TextIO.flushOut TextIO.stdErr)
    7.11        handle _ (*sic*) => ()) ();
    7.12 @@ -79,20 +79,27 @@
    7.13  
    7.14  fun synchronized name lock e =
    7.15    Exn.release (Thread_Attributes.uninterruptible (fn restore_attributes => fn () =>
    7.16 -    let
    7.17 -      val immediate =
    7.18 -        if Mutex.trylock lock then true
    7.19 -        else
    7.20 -          let
    7.21 -            val _ = tracing 5 (fn () => name ^ ": locking ...");
    7.22 -            val timer = Timer.startRealTimer ();
    7.23 -            val _ = Mutex.lock lock;
    7.24 -            val time = Timer.checkRealTimer timer;
    7.25 -            val _ = tracing_time true time (fn () => name ^ ": locked after " ^ Time.toString time);
    7.26 -          in false end;
    7.27 -      val result = Exn.capture (restore_attributes e) ();
    7.28 -      val _ = if immediate then () else tracing 5 (fn () => name ^ ": unlocking ...");
    7.29 -      val _ = Mutex.unlock lock;
    7.30 -    in result end) ());
    7.31 +    if ! trace > 0 then
    7.32 +      let
    7.33 +        val immediate =
    7.34 +          if Mutex.trylock lock then true
    7.35 +          else
    7.36 +            let
    7.37 +              val _ = tracing 5 (fn () => name ^ ": locking ...");
    7.38 +              val timer = Timer.startRealTimer ();
    7.39 +              val _ = Mutex.lock lock;
    7.40 +              val time = Timer.checkRealTimer timer;
    7.41 +              val _ = tracing_time true time (fn () => name ^ ": locked after " ^ Time.toString time);
    7.42 +            in false end;
    7.43 +        val result = Exn.capture (restore_attributes e) ();
    7.44 +        val _ = if immediate then () else tracing 5 (fn () => name ^ ": unlocking ...");
    7.45 +        val _ = Mutex.unlock lock;
    7.46 +      in result end
    7.47 +    else
    7.48 +      let
    7.49 +        val _ = Mutex.lock lock;
    7.50 +        val result = Exn.capture (restore_attributes e) ();
    7.51 +        val _ = Mutex.unlock lock;
    7.52 +      in result end) ());
    7.53  
    7.54  end;
     8.1 --- a/src/Pure/Concurrent/thread_attributes.ML	Thu Dec 15 15:05:35 2016 +0100
     8.2 +++ b/src/Pure/Concurrent/thread_attributes.ML	Fri Dec 16 19:50:46 2016 +0100
     8.3 @@ -88,14 +88,20 @@
     8.4      val w'' = Word.andb (w, Word.notb interrupt_state);
     8.5    in Attributes (if w' = interrupt_asynch then Word.orb (w'', interrupt_asynch_once) else w) end;
     8.6  
     8.7 -end;
     8.8 -
     8.9  fun with_attributes new_atts e =
    8.10    let
    8.11 -    val orig_atts = safe_interrupts (get_attributes ());
    8.12 -    val result = Exn.capture (fn () => (set_attributes (safe_interrupts new_atts); e orig_atts)) ();
    8.13 -    val _ = set_attributes orig_atts;
    8.14 -  in Exn.release result end;
    8.15 +    val atts1 = safe_interrupts (get_attributes ());
    8.16 +    val atts2 = safe_interrupts new_atts;
    8.17 +  in
    8.18 +    if atts1 = atts2 then e atts1
    8.19 +    else
    8.20 +      let
    8.21 +        val result = Exn.capture (fn () => (set_attributes atts2; e atts1)) ();
    8.22 +        val _ = set_attributes atts1;
    8.23 +      in Exn.release result end
    8.24 +  end;
    8.25 +
    8.26 +end;
    8.27  
    8.28  fun uninterruptible f x =
    8.29    with_attributes no_interrupts (fn atts =>
     9.1 --- a/src/Pure/General/source.ML	Thu Dec 15 15:05:35 2016 +0100
     9.2 +++ b/src/Pure/General/source.ML	Fri Dec 16 19:50:46 2016 +0100
     9.3 @@ -14,9 +14,8 @@
     9.4    val map_filter: ('a -> 'b option) -> ('a, 'c) source -> ('b, ('a, 'c) source) source
     9.5    val filter: ('a -> bool) -> ('a, 'b) source -> ('a, ('a, 'b) source) source
     9.6    val of_list: 'a list -> ('a, 'a list) source
     9.7 +  val of_string: string -> (string, string list) source
     9.8    val exhausted: ('a, 'b) source -> ('a, 'a list) source
     9.9 -  val of_string: string -> (string, string list) source
    9.10 -  val of_string_limited: int -> string -> (string, substring) source
    9.11    val source': 'a -> 'b Scan.stopper -> ('a * 'b list -> 'c list * ('a * 'b list)) ->
    9.12      ('b, 'e) source -> ('c, 'a * ('b, 'e) source) source
    9.13    val source: 'a Scan.stopper -> ('a list -> 'b list * 'a list) ->
    9.14 @@ -84,20 +83,9 @@
    9.15  
    9.16  fun of_list xs = make_source [] xs (fn xs => (xs, []));
    9.17  
    9.18 -fun exhausted src = of_list (exhaust src);
    9.19 -
    9.20 -
    9.21 -(* string source *)
    9.22 -
    9.23  val of_string = of_list o raw_explode;
    9.24  
    9.25 -fun of_string_limited limit str =
    9.26 -  make_source [] (Substring.full str)
    9.27 -    (fn s =>
    9.28 -      let
    9.29 -        val (s1, s2) = Substring.splitAt (s, Int.min (Substring.size s, limit));
    9.30 -        val cs = map String.str (Substring.explode s1);
    9.31 -      in (cs, s2) end);
    9.32 +fun exhausted src = of_list (exhaust src);
    9.33  
    9.34  
    9.35  
    10.1 --- a/src/Pure/Isar/proof.ML	Thu Dec 15 15:05:35 2016 +0100
    10.2 +++ b/src/Pure/Isar/proof.ML	Fri Dec 16 19:50:46 2016 +0100
    10.3 @@ -522,8 +522,7 @@
    10.4      fun err_lost () = error ("Lost goal structure:\n" ^ Thm.string_of_thm ctxt goal);
    10.5  
    10.6      val th =
    10.7 -      (Goal.conclude (if length (flat propss) > 1 then Thm.close_derivation goal else goal)
    10.8 -        handle THM _ => err_lost ())
    10.9 +      (Goal.conclude (Thm.close_derivation goal) handle THM _ => err_lost ())
   10.10        |> Drule.flexflex_unique (SOME ctxt)
   10.11        |> Thm.check_shyps ctxt
   10.12        |> Thm.check_hyps (Context.Proof ctxt);
    11.1 --- a/src/Pure/Thy/thy_info.ML	Thu Dec 15 15:05:35 2016 +0100
    11.2 +++ b/src/Pure/Thy/thy_info.ML	Fri Dec 16 19:50:46 2016 +0100
    11.3 @@ -159,7 +159,7 @@
    11.4      (*toplevel proofs and diags*)
    11.5      val _ = Future.join_tasks (maps Future.group_snapshot (Execution.peek exec_id));
    11.6      (*fully nested proofs*)
    11.7 -    val res = Exn.capture Thm.join_theory_proofs theory;
    11.8 +    val res = Exn.capture Thm.consolidate_theory theory;
    11.9    in res :: map Exn.Exn (maps Task_Queue.group_status (Execution.peek exec_id)) end;
   11.10  
   11.11  datatype task =
    12.1 --- a/src/Pure/Tools/thm_deps.ML	Thu Dec 15 15:05:35 2016 +0100
    12.2 +++ b/src/Pure/Tools/thm_deps.ML	Fri Dec 16 19:50:46 2016 +0100
    12.3 @@ -20,8 +20,8 @@
    12.4      fun make_node name directory =
    12.5        Graph_Display.session_node
    12.6         {name = Long_Name.base_name name, directory = directory, unfold = false, path = ""};
    12.7 -    fun add_dep ("", _, _) = I
    12.8 -      | add_dep (name, _, PBody {thms = thms', ...}) =
    12.9 +    fun add_dep {name = "", ...} = I
   12.10 +      | add_dep {name = name, body = PBody {thms = thms', ...}, ...} =
   12.11            let
   12.12              val prefix = #1 (split_last (Long_Name.explode name));
   12.13              val session =
   12.14 @@ -35,7 +35,7 @@
   12.15                    | NONE => [])
   12.16                | _ => ["global"]);
   12.17              val node = make_node name (space_implode "/" (session @ prefix));
   12.18 -            val deps = filter_out (fn s => s = "") (map (#1 o #2) thms');
   12.19 +            val deps = filter_out (fn s => s = "") (map (Proofterm.thm_node_name o #2) thms');
   12.20            in Symtab.update (name, (node, deps)) end;
   12.21      val entries0 = Proofterm.fold_body_thms add_dep (Thm.proof_bodies_of thms) Symtab.empty;
   12.22      val entries1 =
   12.23 @@ -73,7 +73,7 @@
   12.24  
   12.25      val used =
   12.26        Proofterm.fold_body_thms
   12.27 -        (fn (a, _, _) => a <> "" ? Symtab.update (a, ()))
   12.28 +        (fn {name = a, ...} => a <> "" ? Symtab.update (a, ()))
   12.29          (map Proofterm.strip_thm (Thm.proof_bodies_of (map (#1 o #2) new_thms)))
   12.30          Symtab.empty;
   12.31  
    13.1 --- a/src/Pure/goal.ML	Thu Dec 15 15:05:35 2016 +0100
    13.2 +++ b/src/Pure/goal.ML	Fri Dec 16 19:50:46 2016 +0100
    13.3 @@ -232,7 +232,7 @@
    13.4            (Thm.term_of stmt);
    13.5    in
    13.6      res
    13.7 -    |> length props > 1 ? Thm.close_derivation
    13.8 +    |> Thm.close_derivation
    13.9      |> Conjunction.elim_balanced (length props)
   13.10      |> map (Assumption.export false ctxt' ctxt)
   13.11      |> Variable.export ctxt' ctxt
    14.1 --- a/src/Pure/more_thm.ML	Thu Dec 15 15:05:35 2016 +0100
    14.2 +++ b/src/Pure/more_thm.ML	Fri Dec 16 19:50:46 2016 +0100
    14.3 @@ -111,7 +111,7 @@
    14.4    val untag: string -> attribute
    14.5    val kind: string -> attribute
    14.6    val register_proofs: thm list -> theory -> theory
    14.7 -  val join_theory_proofs: theory -> unit
    14.8 +  val consolidate_theory: theory -> unit
    14.9    val show_consts_raw: Config.raw
   14.10    val show_consts: bool Config.T
   14.11    val show_hyps_raw: Config.raw
   14.12 @@ -452,8 +452,7 @@
   14.13  (* close_derivation *)
   14.14  
   14.15  fun close_derivation thm =
   14.16 -  if Thm.derivation_name thm = "" then Thm.name_derivation "" thm
   14.17 -  else thm;
   14.18 +  if Thm.derivation_closed thm then thm else Thm.name_derivation "" thm;
   14.19  
   14.20  
   14.21  (* user renaming of parameters in a subgoal *)
   14.22 @@ -645,8 +644,8 @@
   14.23  fun register_proofs more_thms =
   14.24    Proofs.map (fold (cons o Thm.trim_context) more_thms);
   14.25  
   14.26 -fun join_theory_proofs thy =
   14.27 -  Thm.join_proofs (map (Thm.transfer thy) (rev (Proofs.get thy)));
   14.28 +fun consolidate_theory thy =
   14.29 +  List.app (Thm.consolidate o Thm.transfer thy) (rev (Proofs.get thy));
   14.30  
   14.31  
   14.32  
    15.1 --- a/src/Pure/proofterm.ML	Thu Dec 15 15:05:35 2016 +0100
    15.2 +++ b/src/Pure/proofterm.ML	Fri Dec 16 19:50:46 2016 +0100
    15.3 @@ -10,6 +10,7 @@
    15.4  sig
    15.5    val proofs: int Unsynchronized.ref
    15.6  
    15.7 +  type thm_node
    15.8    datatype proof =
    15.9       MinProof
   15.10     | PBound of int
   15.11 @@ -25,7 +26,7 @@
   15.12     | PThm of serial * ((string * term * typ list option) * proof_body future)
   15.13    and proof_body = PBody of
   15.14      {oracles: (string * term) Ord_List.T,
   15.15 -     thms: (serial * (string * term * proof_body future)) Ord_List.T,
   15.16 +     thms: (serial * thm_node) Ord_List.T,
   15.17       proof: proof}
   15.18  
   15.19    val %> : proof * term -> proof
   15.20 @@ -35,13 +36,17 @@
   15.21  sig
   15.22    include BASIC_PROOFTERM
   15.23  
   15.24 +  type pthm = serial * thm_node
   15.25    type oracle = string * term
   15.26 -  type pthm = serial * (string * term * proof_body future)
   15.27    val proof_of: proof_body -> proof
   15.28 +  val thm_node_name: thm_node -> string
   15.29 +  val thm_node_prop: thm_node -> term
   15.30 +  val thm_node_body: thm_node -> proof_body future
   15.31    val join_proof: proof_body future -> proof
   15.32    val fold_proof_atoms: bool -> (proof -> 'a -> 'a) -> proof list -> 'a -> 'a
   15.33 -  val fold_body_thms: (string * term * proof_body -> 'a -> 'a) -> proof_body list -> 'a -> 'a
   15.34 -  val join_bodies: proof_body list -> unit
   15.35 +  val fold_body_thms: ({serial: serial, name: string, prop: term, body: proof_body} -> 'a -> 'a) ->
   15.36 +    proof_body list -> 'a -> 'a
   15.37 +  val consolidate: proof_body -> unit
   15.38    val peek_status: proof_body list -> {failed: bool, oracle: bool, unfinished: bool}
   15.39  
   15.40    val oracle_ord: oracle * oracle -> order
   15.41 @@ -60,6 +65,8 @@
   15.42  
   15.43    (** primitive operations **)
   15.44    val proofs_enabled: unit -> bool
   15.45 +  val atomic_proof: proof -> bool
   15.46 +  val compact_proof: proof -> bool
   15.47    val proof_combt: proof * term list -> proof
   15.48    val proof_combt': proof * term option list -> proof
   15.49    val proof_combP: proof * proof list -> proof
   15.50 @@ -173,16 +180,35 @@
   15.51   | PThm of serial * ((string * term * typ list option) * proof_body future)
   15.52  and proof_body = PBody of
   15.53    {oracles: (string * term) Ord_List.T,
   15.54 -   thms: (serial * (string * term * proof_body future)) Ord_List.T,
   15.55 -   proof: proof};
   15.56 +   thms: (serial * thm_node) Ord_List.T,
   15.57 +   proof: proof}
   15.58 +and thm_node =
   15.59 +  Thm_Node of {name: string, prop: term, body: proof_body future, consolidate: unit lazy};
   15.60  
   15.61  type oracle = string * term;
   15.62 -type pthm = serial * (string * term * proof_body future);
   15.63 +type pthm = serial * thm_node;
   15.64  
   15.65  fun proof_of (PBody {proof, ...}) = proof;
   15.66  val join_proof = Future.join #> proof_of;
   15.67  
   15.68 -fun join_thms (thms: pthm list) = ignore (Future.joins (map (#3 o #2) thms));
   15.69 +fun rep_thm_node (Thm_Node args) = args;
   15.70 +val thm_node_name = #name o rep_thm_node;
   15.71 +val thm_node_prop = #prop o rep_thm_node;
   15.72 +val thm_node_body = #body o rep_thm_node;
   15.73 +val thm_node_consolidate = #consolidate o rep_thm_node;
   15.74 +
   15.75 +fun join_thms (thms: pthm list) =
   15.76 +  Future.joins (map (thm_node_body o #2) thms);
   15.77 +
   15.78 +fun consolidate (PBody {thms, ...}) =
   15.79 +  List.app (Lazy.force o thm_node_consolidate o #2) thms;
   15.80 +
   15.81 +fun make_thm_node name prop body =
   15.82 +  Thm_Node {name = name, prop = prop, body = body,
   15.83 +    consolidate =
   15.84 +      Lazy.lazy (fn () =>
   15.85 +        let val PBody {thms, ...} = Future.join body
   15.86 +        in List.app consolidate (join_thms thms) end)};
   15.87  
   15.88  
   15.89  (***** proof atoms *****)
   15.90 @@ -205,27 +231,27 @@
   15.91  fun fold_body_thms f =
   15.92    let
   15.93      fun app (PBody {thms, ...}) =
   15.94 -      tap join_thms thms |> fold (fn (i, (name, prop, body)) => fn (x, seen) =>
   15.95 +      tap join_thms thms |> fold (fn (i, thm_node) => fn (x, seen) =>
   15.96          if Inttab.defined seen i then (x, seen)
   15.97          else
   15.98            let
   15.99 -            val body' = Future.join body;
  15.100 -            val (x', seen') = app body' (x, Inttab.update (i, ()) seen);
  15.101 -          in (f (name, prop, body') x', seen') end);
  15.102 +            val name = thm_node_name thm_node;
  15.103 +            val prop = thm_node_prop thm_node;
  15.104 +            val body = Future.join (thm_node_body thm_node);
  15.105 +            val (x', seen') = app body (x, Inttab.update (i, ()) seen);
  15.106 +          in (f {serial = i, name = name, prop = prop, body = body} x', seen') end);
  15.107    in fn bodies => fn x => #1 (fold app bodies (x, Inttab.empty)) end;
  15.108  
  15.109 -fun join_bodies bodies = fold_body_thms (fn _ => fn () => ()) bodies ();
  15.110 -
  15.111  fun peek_status bodies =
  15.112    let
  15.113      fun status (PBody {oracles, thms, ...}) x =
  15.114        let
  15.115          val ((oracle, unfinished, failed), seen) =
  15.116 -          (thms, x) |-> fold (fn (i, (_, _, body)) => fn (st, seen) =>
  15.117 +          (thms, x) |-> fold (fn (i, thm_node) => fn (st, seen) =>
  15.118              if Inttab.defined seen i then (st, seen)
  15.119              else
  15.120                let val seen' = Inttab.update (i, ()) seen in
  15.121 -                (case Future.peek body of
  15.122 +                (case Future.peek (thm_node_body thm_node) of
  15.123                    SOME (Exn.Res body') => status body' (st, seen')
  15.124                  | SOME (Exn.Exn _) =>
  15.125                      let val (oracle, unfinished, _) = st
  15.126 @@ -243,7 +269,7 @@
  15.127  (* proof body *)
  15.128  
  15.129  val oracle_ord = prod_ord fast_string_ord Term_Ord.fast_term_ord;
  15.130 -fun thm_ord ((i, _): pthm, (j, _)) = int_ord (j, i);
  15.131 +fun thm_ord ((i, _): pthm, (j, _): pthm) = int_ord (j, i);
  15.132  
  15.133  val unions_oracles = Ord_List.unions oracle_ord;
  15.134  val unions_thms = Ord_List.unions thm_ord;
  15.135 @@ -251,12 +277,12 @@
  15.136  val all_oracles_of =
  15.137    let
  15.138      fun collect (PBody {oracles, thms, ...}) =
  15.139 -      tap join_thms thms |> fold (fn (i, (_, _, body)) => fn (x, seen) =>
  15.140 +      tap join_thms thms |> fold (fn (i, thm_node) => fn (x, seen) =>
  15.141          if Inttab.defined seen i then (x, seen)
  15.142          else
  15.143            let
  15.144 -            val body' = Future.join body;
  15.145 -            val (x', seen') = collect body' (x, Inttab.update (i, ()) seen);
  15.146 +            val body = Future.join (thm_node_body thm_node);
  15.147 +            val (x', seen') = collect body (x, Inttab.update (i, ()) seen);
  15.148            in (if null oracles then x' else oracles :: x', seen') end);
  15.149    in fn body => unions_oracles (#1 (collect body ([], Inttab.empty))) end;
  15.150  
  15.151 @@ -264,7 +290,7 @@
  15.152    let
  15.153      val (oracles, thms) = fold_proof_atoms false
  15.154        (fn Oracle (s, prop, _) => apfst (cons (s, prop))
  15.155 -        | PThm (i, ((name, prop, _), body)) => apsnd (cons (i, (name, prop, body)))
  15.156 +        | PThm (i, ((name, prop, _), body)) => apsnd (cons (i, make_thm_node name prop body))
  15.157          | _ => I) [prf] ([], []);
  15.158    in
  15.159      PBody
  15.160 @@ -308,8 +334,9 @@
  15.161      ([int_atom a, b], triple term (option (list typ)) proof_body (c, d, Future.join body))]
  15.162  and proof_body (PBody {oracles, thms, proof = prf}) =
  15.163    triple (list (pair string term)) (list pthm) proof (oracles, thms, prf)
  15.164 -and pthm (a, (b, c, body)) =
  15.165 -  pair int (triple string term proof_body) (a, (b, c, Future.join body));
  15.166 +and pthm (a, thm_node) =
  15.167 +  pair int (triple string term proof_body)
  15.168 +    (a, (thm_node_name thm_node, thm_node_prop thm_node, Future.join (thm_node_body thm_node)));
  15.169  
  15.170  in
  15.171  
  15.172 @@ -345,7 +372,7 @@
  15.173    in PBody {oracles = a, thms = b, proof = c} end
  15.174  and pthm x =
  15.175    let val (a, (b, c, d)) = pair int (triple string term proof_body) x
  15.176 -  in (a, (b, c, Future.value d)) end;
  15.177 +  in (a, make_thm_node b c (Future.value d)) end;
  15.178  
  15.179  in
  15.180  
  15.181 @@ -357,6 +384,19 @@
  15.182  
  15.183  (***** proof objects with different levels of detail *****)
  15.184  
  15.185 +fun atomic_proof prf =
  15.186 +  (case prf of
  15.187 +    Abst _ => false
  15.188 +  | AbsP _ => false
  15.189 +  | op % _ => false
  15.190 +  | op %% _ => false
  15.191 +  | Promise _ => false
  15.192 +  | _ => true);
  15.193 +
  15.194 +fun compact_proof (prf % _) = compact_proof prf
  15.195 +  | compact_proof (prf1 %% prf2) = atomic_proof prf2 andalso compact_proof prf1
  15.196 +  | compact_proof prf = atomic_proof prf;
  15.197 +
  15.198  fun (prf %> t) = prf % SOME t;
  15.199  
  15.200  val proof_combt = Library.foldl (op %>);
  15.201 @@ -533,11 +573,13 @@
  15.202        prf_add_loose_bnos plev tlev prf2
  15.203          (prf_add_loose_bnos plev tlev prf1 p)
  15.204    | prf_add_loose_bnos plev tlev (prf % opt) (is, js) =
  15.205 -      prf_add_loose_bnos plev tlev prf (case opt of
  15.206 +      prf_add_loose_bnos plev tlev prf
  15.207 +        (case opt of
  15.208            NONE => (is, insert (op =) ~1 js)
  15.209          | SOME t => (is, add_loose_bnos (t, tlev, js)))
  15.210    | prf_add_loose_bnos plev tlev (AbsP (_, opt, prf)) (is, js) =
  15.211 -      prf_add_loose_bnos (plev+1) tlev prf (case opt of
  15.212 +      prf_add_loose_bnos (plev+1) tlev prf
  15.213 +        (case opt of
  15.214            NONE => (is, insert (op =) ~1 js)
  15.215          | SOME t => (is, add_loose_bnos (t, tlev, js)))
  15.216    | prf_add_loose_bnos plev tlev (Abst (_, _, prf)) p =
  15.217 @@ -635,7 +677,7 @@
  15.218            handle Same.SAME => prf % Same.map_option (subst' lev) t)
  15.219        | subst _ _ = raise Same.SAME
  15.220      and substh lev prf = (subst lev prf handle Same.SAME => prf);
  15.221 -  in case args of [] => prf | _ => substh 0 prf end;
  15.222 +  in (case args of [] => prf | _ => substh 0 prf) end;
  15.223  
  15.224  fun prf_subst_pbounds args prf =
  15.225    let
  15.226 @@ -651,7 +693,7 @@
  15.227        | subst (prf % t) Plev tlev = subst prf Plev tlev % t
  15.228        | subst  _ _ _ = raise Same.SAME
  15.229      and substh prf Plev tlev = (subst prf Plev tlev handle Same.SAME => prf)
  15.230 -  in case args of [] => prf | _ => substh prf 0 0 end;
  15.231 +  in (case args of [] => prf | _ => substh prf 0 0) end;
  15.232  
  15.233  
  15.234  (**** Freezing and thawing of variables in proof terms ****)
  15.235 @@ -992,7 +1034,7 @@
  15.236          | Var _ => SOME (remove_types t)
  15.237          | _ => NONE) %
  15.238          (case head_of g of
  15.239 -           Abs _ => SOME (remove_types u)
  15.240 +          Abs _ => SOME (remove_types u)
  15.241          | Var _ => SOME (remove_types u)
  15.242          | _ => NONE) %% prf1 %% prf2
  15.243       | _ => prf % NONE % NONE %% prf1 %% prf2)
  15.244 @@ -1105,7 +1147,8 @@
  15.245        add_npvars q p Ts (vs, if p andalso q then betapply (t, Var (("",0), T)) else t)
  15.246    | add_npvars q p Ts (vs, Abs (_, T, t)) = add_npvars q p (T::Ts) (vs, t)
  15.247    | add_npvars _ _ Ts (vs, t) = add_npvars' Ts (vs, t)
  15.248 -and add_npvars' Ts (vs, t) = (case strip_comb t of
  15.249 +and add_npvars' Ts (vs, t) =
  15.250 +  (case strip_comb t of
  15.251      (Var (ixn, _), ts) => if test_args [] ts then vs
  15.252        else Library.foldl (add_npvars' Ts)
  15.253          (AList.update (op =) (ixn,
  15.254 @@ -1115,19 +1158,20 @@
  15.255  
  15.256  fun prop_vars (Const ("Pure.imp", _) $ P $ Q) = union (op =) (prop_vars P) (prop_vars Q)
  15.257    | prop_vars (Const ("Pure.all", _) $ Abs (_, _, t)) = prop_vars t
  15.258 -  | prop_vars t = (case strip_comb t of
  15.259 -      (Var (ixn, _), _) => [ixn] | _ => []);
  15.260 +  | prop_vars t = (case strip_comb t of (Var (ixn, _), _) => [ixn] | _ => []);
  15.261  
  15.262  fun is_proj t =
  15.263    let
  15.264 -    fun is_p i t = (case strip_comb t of
  15.265 +    fun is_p i t =
  15.266 +      (case strip_comb t of
  15.267          (Bound _, []) => false
  15.268        | (Bound j, ts) => j >= i orelse exists (is_p i) ts
  15.269        | (Abs (_, _, u), _) => is_p (i+1) u
  15.270        | (_, ts) => exists (is_p i) ts)
  15.271 -  in (case strip_abs_body t of
  15.272 -        Bound _ => true
  15.273 -      | t' => is_p 0 t')
  15.274 +  in
  15.275 +    (case strip_abs_body t of
  15.276 +      Bound _ => true
  15.277 +    | t' => is_p 0 t')
  15.278    end;
  15.279  
  15.280  fun needed_vars prop =
  15.281 @@ -1196,7 +1240,8 @@
  15.282              val (ts', ts'') = chop (length vs) ts;
  15.283              val insts = take (length ts') (map (fst o dest_Var) vs) ~~ ts';
  15.284              val nvs = Library.foldl (fn (ixns', (ixn, ixns)) =>
  15.285 -              insert (op =) ixn (case AList.lookup (op =) insts ixn of
  15.286 +              insert (op =) ixn
  15.287 +                (case AList.lookup (op =) insts ixn of
  15.288                    SOME (SOME t) => if is_proj t then union (op =) ixns ixns' else ixns'
  15.289                  | _ => union (op =) ixns ixns'))
  15.290                    (needed prop ts'' prfs, add_npvars false true [] ([], prop));
  15.291 @@ -1250,12 +1295,12 @@
  15.292  
  15.293      fun mtch Ts i j (pinst, tinst) (Hyp (Var (ixn, _)), prf) =
  15.294            if i = 0 andalso j = 0 then ((ixn, prf) :: pinst, tinst)
  15.295 -          else (case apfst (flt i) (apsnd (flt j)
  15.296 -                  (prf_add_loose_bnos 0 0 prf ([], []))) of
  15.297 +          else
  15.298 +            (case apfst (flt i) (apsnd (flt j) (prf_add_loose_bnos 0 0 prf ([], []))) of
  15.299                ([], []) => ((ixn, incr_pboundvars (~i) (~j) prf) :: pinst, tinst)
  15.300 -            | ([], _) => if j = 0 then
  15.301 -                   ((ixn, incr_pboundvars (~i) (~j) prf) :: pinst, tinst)
  15.302 -                 else raise PMatch
  15.303 +            | ([], _) =>
  15.304 +                if j = 0 then ((ixn, incr_pboundvars (~i) (~j) prf) :: pinst, tinst)
  15.305 +                else raise PMatch
  15.306              | _ => raise PMatch)
  15.307        | mtch Ts i j inst (prf1 % opt1, prf2 % opt2) =
  15.308            optmatch (matcht Ts j) (mtch Ts i j inst (prf1, prf2)) (opt1, opt2)
  15.309 @@ -1389,45 +1434,57 @@
  15.310        | rew0 Ts hs prf = rew Ts hs prf;
  15.311  
  15.312      fun rew1 _ _ (Hyp (Var _)) _ = NONE
  15.313 -      | rew1 Ts hs skel prf = (case rew2 Ts hs skel prf of
  15.314 -          SOME prf1 => (case rew0 Ts hs prf1 of
  15.315 -              SOME (prf2, skel') => SOME (the_default prf2 (rew1 Ts hs skel' prf2))
  15.316 -            | NONE => SOME prf1)
  15.317 -        | NONE => (case rew0 Ts hs prf of
  15.318 -              SOME (prf1, skel') => SOME (the_default prf1 (rew1 Ts hs skel' prf1))
  15.319 -            | NONE => NONE))
  15.320 +      | rew1 Ts hs skel prf =
  15.321 +          (case rew2 Ts hs skel prf of
  15.322 +            SOME prf1 =>
  15.323 +              (case rew0 Ts hs prf1 of
  15.324 +                SOME (prf2, skel') => SOME (the_default prf2 (rew1 Ts hs skel' prf2))
  15.325 +              | NONE => SOME prf1)
  15.326 +          | NONE =>
  15.327 +              (case rew0 Ts hs prf of
  15.328 +                SOME (prf1, skel') => SOME (the_default prf1 (rew1 Ts hs skel' prf1))
  15.329 +              | NONE => NONE))
  15.330  
  15.331 -    and rew2 Ts hs skel (prf % SOME t) = (case prf of
  15.332 +    and rew2 Ts hs skel (prf % SOME t) =
  15.333 +          (case prf of
  15.334              Abst (_, _, body) =>
  15.335                let val prf' = prf_subst_bounds [t] body
  15.336                in SOME (the_default prf' (rew2 Ts hs no_skel prf')) end
  15.337 -          | _ => (case rew1 Ts hs (case skel of skel' % _ => skel' | _ => no_skel) prf of
  15.338 -              SOME prf' => SOME (prf' % SOME t)
  15.339 -            | NONE => NONE))
  15.340 +          | _ =>
  15.341 +              (case rew1 Ts hs (case skel of skel' % _ => skel' | _ => no_skel) prf of
  15.342 +                SOME prf' => SOME (prf' % SOME t)
  15.343 +              | NONE => NONE))
  15.344        | rew2 Ts hs skel (prf % NONE) = Option.map (fn prf' => prf' % NONE)
  15.345            (rew1 Ts hs (case skel of skel' % _ => skel' | _ => no_skel) prf)
  15.346 -      | rew2 Ts hs skel (prf1 %% prf2) = (case prf1 of
  15.347 +      | rew2 Ts hs skel (prf1 %% prf2) =
  15.348 +          (case prf1 of
  15.349              AbsP (_, _, body) =>
  15.350                let val prf' = prf_subst_pbounds [prf2] body
  15.351                in SOME (the_default prf' (rew2 Ts hs no_skel prf')) end
  15.352            | _ =>
  15.353 -            let val (skel1, skel2) = (case skel of
  15.354 -                skel1 %% skel2 => (skel1, skel2)
  15.355 -              | _ => (no_skel, no_skel))
  15.356 -            in case rew1 Ts hs skel1 prf1 of
  15.357 -                SOME prf1' => (case rew1 Ts hs skel2 prf2 of
  15.358 +            let
  15.359 +              val (skel1, skel2) =
  15.360 +                (case skel of
  15.361 +                  skel1 %% skel2 => (skel1, skel2)
  15.362 +                | _ => (no_skel, no_skel))
  15.363 +            in
  15.364 +              (case rew1 Ts hs skel1 prf1 of
  15.365 +                SOME prf1' =>
  15.366 +                  (case rew1 Ts hs skel2 prf2 of
  15.367                      SOME prf2' => SOME (prf1' %% prf2')
  15.368                    | NONE => SOME (prf1' %% prf2))
  15.369 -              | NONE => (case rew1 Ts hs skel2 prf2 of
  15.370 +              | NONE =>
  15.371 +                  (case rew1 Ts hs skel2 prf2 of
  15.372                      SOME prf2' => SOME (prf1 %% prf2')
  15.373 -                  | NONE => NONE)
  15.374 +                  | NONE => NONE))
  15.375              end)
  15.376 -      | rew2 Ts hs skel (Abst (s, T, prf)) = (case rew1 (the_default dummyT T :: Ts) hs
  15.377 +      | rew2 Ts hs skel (Abst (s, T, prf)) =
  15.378 +          (case rew1 (the_default dummyT T :: Ts) hs
  15.379                (case skel of Abst (_, _, skel') => skel' | _ => no_skel) prf of
  15.380              SOME prf' => SOME (Abst (s, T, prf'))
  15.381            | NONE => NONE)
  15.382 -      | rew2 Ts hs skel (AbsP (s, t, prf)) = (case rew1 Ts (t :: hs)
  15.383 -              (case skel of AbsP (_, _, skel') => skel' | _ => no_skel) prf of
  15.384 +      | rew2 Ts hs skel (AbsP (s, t, prf)) =
  15.385 +          (case rew1 Ts (t :: hs) (case skel of AbsP (_, _, skel') => skel' | _ => no_skel) prf of
  15.386              SOME prf' => SOME (AbsP (s, t, prf'))
  15.387            | NONE => NONE)
  15.388        | rew2 _ _ _ _ = NONE;
  15.389 @@ -1476,6 +1533,8 @@
  15.390  
  15.391  fun fulfill_norm_proof thy ps body0 =
  15.392    let
  15.393 +    val _ = List.app (consolidate o #2) ps;
  15.394 +    val _ = consolidate body0;
  15.395      val PBody {oracles = oracles0, thms = thms0, proof = proof0} = body0;
  15.396      val oracles =
  15.397        unions_oracles
  15.398 @@ -1573,15 +1632,14 @@
  15.399            else new_prf ()
  15.400        | _ => new_prf ());
  15.401      val head = PThm (i, ((name, prop1, NONE), body'));
  15.402 -  in ((i, (name, prop1, body')), head, args, argsP, args1) end;
  15.403 +  in ((i, make_thm_node name prop1 body'), head, args, argsP, args1) end;
  15.404  
  15.405  fun thm_proof thy name shyps hyps concl promises body =
  15.406    let val (pthm, head, args, argsP, _) = prepare_thm_proof thy name shyps hyps concl promises body
  15.407    in (pthm, proof_combP (proof_combt' (head, args), argsP)) end;
  15.408  
  15.409  fun unconstrain_thm_proof thy shyps concl promises body =
  15.410 -  let
  15.411 -    val (pthm, head, _, _, args) = prepare_thm_proof thy "" shyps [] concl promises body
  15.412 +  let val (pthm, head, _, _, args) = prepare_thm_proof thy "" shyps [] concl promises body
  15.413    in (pthm, proof_combt' (head, args)) end;
  15.414  
  15.415  
    16.1 --- a/src/Pure/thm.ML	Thu Dec 15 15:05:35 2016 +0100
    16.2 +++ b/src/Pure/thm.ML	Fri Dec 16 19:50:46 2016 +0100
    16.3 @@ -86,9 +86,10 @@
    16.4    val proof_bodies_of: thm list -> proof_body list
    16.5    val proof_body_of: thm -> proof_body
    16.6    val proof_of: thm -> proof
    16.7 -  val join_proofs: thm list -> unit
    16.8 +  val consolidate: thm -> unit
    16.9    val peek_status: thm -> {oracle: bool, unfinished: bool, failed: bool}
   16.10    val future: thm future -> cterm -> thm
   16.11 +  val derivation_closed: thm -> bool
   16.12    val derivation_name: thm -> string
   16.13    val name_derivation: string -> thm -> thm
   16.14    val axiom: theory -> string -> thm
   16.15 @@ -584,21 +585,14 @@
   16.16  and join_promises_of thms = join_promises (Ord_List.make promise_ord (maps raw_promises_of thms));
   16.17  
   16.18  fun fulfill_body (th as Thm (Deriv {promises, body}, _)) =
   16.19 -  Proofterm.fulfill_norm_proof (theory_of_thm th) (fulfill_promises promises) body
   16.20 -and fulfill_promises promises =
   16.21 -  map fst promises ~~ map fulfill_body (Future.joins (map snd promises));
   16.22 +  let val fulfilled_promises = map #1 promises ~~ map fulfill_body (Future.joins (map #2 promises))
   16.23 +  in Proofterm.fulfill_norm_proof (theory_of_thm th) fulfilled_promises body end;
   16.24  
   16.25 -fun proof_bodies_of thms =
   16.26 -  let
   16.27 -    val _ = join_promises_of thms;
   16.28 -    val bodies = map fulfill_body thms;
   16.29 -    val _ = Proofterm.join_bodies bodies;
   16.30 -  in bodies end;
   16.31 -
   16.32 +fun proof_bodies_of thms = (join_promises_of thms; map fulfill_body thms);
   16.33  val proof_body_of = singleton proof_bodies_of;
   16.34  val proof_of = Proofterm.proof_of o proof_body_of;
   16.35  
   16.36 -val join_proofs = ignore o proof_bodies_of;
   16.37 +val consolidate = ignore o proof_bodies_of o single;
   16.38  
   16.39  
   16.40  (* derivation status *)
   16.41 @@ -655,6 +649,10 @@
   16.42  (* closed derivations with official name *)
   16.43  
   16.44  (*non-deterministic, depends on unknown promises*)
   16.45 +fun derivation_closed (Thm (Deriv {body, ...}, _)) =
   16.46 +  Proofterm.compact_proof (Proofterm.proof_of body);
   16.47 +
   16.48 +(*non-deterministic, depends on unknown promises*)
   16.49  fun derivation_name (Thm (Deriv {body, ...}, {shyps, hyps, prop, ...})) =
   16.50    Proofterm.get_name shyps hyps prop (Proofterm.proof_of body);
   16.51  
   16.52 @@ -1305,9 +1303,9 @@
   16.53      val _ = null tfrees orelse err ("illegal free type variables " ^ commas_quote tfrees);
   16.54  
   16.55      val ps = map (apsnd (Future.map fulfill_body)) promises;
   16.56 -    val (pthm as (_, (_, prop', _)), proof) =
   16.57 -      Proofterm.unconstrain_thm_proof thy shyps prop ps body;
   16.58 +    val (pthm, proof) = Proofterm.unconstrain_thm_proof thy shyps prop ps body;
   16.59      val der' = make_deriv [] [] [pthm] proof;
   16.60 +    val prop' = Proofterm.thm_node_prop (#2 pthm);
   16.61    in
   16.62      Thm (der',
   16.63       {cert = cert,