always close derivation, for significantly improved performance without parallel proofs;
authorwenzelm
Wed Dec 14 16:59:41 2016 +0100 (2016-12-14)
changeset 645677141a3a4dc83
parent 64566 679710d324f1
child 64568 a504a3dec35a
always close derivation, for significantly improved performance without parallel proofs;
src/Pure/Isar/proof.ML
src/Pure/goal.ML
     1.1 --- a/src/Pure/Isar/proof.ML	Wed Dec 14 15:48:18 2016 +0100
     1.2 +++ b/src/Pure/Isar/proof.ML	Wed Dec 14 16:59:41 2016 +0100
     1.3 @@ -522,8 +522,7 @@
     1.4      fun err_lost () = error ("Lost goal structure:\n" ^ Thm.string_of_thm ctxt goal);
     1.5  
     1.6      val th =
     1.7 -      (Goal.conclude (if length (flat propss) > 1 then Thm.close_derivation goal else goal)
     1.8 -        handle THM _ => err_lost ())
     1.9 +      (Goal.conclude (Thm.close_derivation goal) handle THM _ => err_lost ())
    1.10        |> Drule.flexflex_unique (SOME ctxt)
    1.11        |> Thm.check_shyps ctxt
    1.12        |> Thm.check_hyps (Context.Proof ctxt);
     2.1 --- a/src/Pure/goal.ML	Wed Dec 14 15:48:18 2016 +0100
     2.2 +++ b/src/Pure/goal.ML	Wed Dec 14 16:59:41 2016 +0100
     2.3 @@ -232,7 +232,7 @@
     2.4            (Thm.term_of stmt);
     2.5    in
     2.6      res
     2.7 -    |> length props > 1 ? Thm.close_derivation
     2.8 +    |> Thm.close_derivation
     2.9      |> Conjunction.elim_balanced (length props)
    2.10      |> map (Assumption.export false ctxt' ctxt)
    2.11      |> Variable.export ctxt' ctxt