more aggressive compaction of multi-goal proof terms (see also a8babbb6d5ea, 4dd0ba632e40);
authorwenzelm
Tue Jul 14 19:01:46 2015 +0200 (2015-07-14)
changeset 60723757cad5a3fe9
parent 60722 a8babbb6d5ea
child 60724 4fce5d462afc
more aggressive compaction of multi-goal proof terms (see also a8babbb6d5ea, 4dd0ba632e40);
src/Pure/Isar/proof.ML
src/Pure/goal.ML
     1.1 --- a/src/Pure/Isar/proof.ML	Tue Jul 14 11:29:43 2015 +0200
     1.2 +++ b/src/Pure/Isar/proof.ML	Tue Jul 14 19:01:46 2015 +0200
     1.3 @@ -498,7 +498,7 @@
     1.4      fun err_lost () = error ("Lost goal structure:\n" ^ Display.string_of_thm ctxt goal);
     1.5  
     1.6      val th =
     1.7 -      (Goal.conclude (if length (flat propss) > 1 then Thm.norm_proof goal else goal)
     1.8 +      (Goal.conclude (if length (flat propss) > 1 then Thm.close_derivation goal else goal)
     1.9          handle THM _ => err_lost ())
    1.10        |> Drule.flexflex_unique (SOME ctxt)
    1.11        |> Thm.check_shyps (Variable.sorts_of ctxt)
     2.1 --- a/src/Pure/goal.ML	Tue Jul 14 11:29:43 2015 +0200
     2.2 +++ b/src/Pure/goal.ML	Tue Jul 14 19:01:46 2015 +0200
     2.3 @@ -231,7 +231,7 @@
     2.4            (Thm.term_of stmt);
     2.5    in
     2.6      res
     2.7 -    |> length props > 1 ? Thm.norm_proof
     2.8 +    |> length props > 1 ? Thm.close_derivation
     2.9      |> Conjunction.elim_balanced (length props)
    2.10      |> map (Assumption.export false ctxt' ctxt)
    2.11      |> Variable.export ctxt' ctxt