proper adjust_maxidx: assms could have maxidx >= 0, e.g. from command "subgoal premises";
authorwenzelm
Fri Jul 27 17:32:16 2018 +0200 (12 months ago)
changeset 68693a9bef20b1e47
parent 68692 0c568ec56f37
child 68694 03e104be99af
proper adjust_maxidx: assms could have maxidx >= 0, e.g. from command "subgoal premises";
src/Pure/goal.ML
     1.1 --- a/src/Pure/goal.ML	Fri Jul 27 17:27:42 2018 +0200
     1.2 +++ b/src/Pure/goal.ML	Fri Jul 27 17:32:16 2018 +0200
     1.3 @@ -129,9 +129,9 @@
     1.4        |> Thm.weaken_sorts' ctxt;
     1.5      val global_result = result |> Future.map
     1.6        (Drule.flexflex_unique (SOME ctxt) #>
     1.7 -        Thm.adjust_maxidx_thm ~1 #>
     1.8          Drule.implies_intr_list assms #>
     1.9          Drule.forall_intr_list fixes #>
    1.10 +        Thm.adjust_maxidx_thm ~1 #>
    1.11          Thm.generalize (map #1 tfrees, []) 0 #>
    1.12          Thm.strip_shyps);
    1.13      val local_result =