# HG changeset patch
# User wenzelm
# Date 1532705536 -7200
# Node ID a9bef20b1e476d41276cdfe289508eb5cbe61321
# Parent  0c568ec56f3705b1e04fda7b2122d404ce7a3545
proper adjust_maxidx: assms could have maxidx >= 0, e.g. from command "subgoal premises";

diff -r 0c568ec56f37 -r a9bef20b1e47 src/Pure/goal.ML
--- a/src/Pure/goal.ML	Fri Jul 27 17:27:42 2018 +0200
+++ b/src/Pure/goal.ML	Fri Jul 27 17:32:16 2018 +0200
@@ -129,9 +129,9 @@
       |> Thm.weaken_sorts' ctxt;
     val global_result = result |> Future.map
       (Drule.flexflex_unique (SOME ctxt) #>
-        Thm.adjust_maxidx_thm ~1 #>
         Drule.implies_intr_list assms #>
         Drule.forall_intr_list fixes #>
+        Thm.adjust_maxidx_thm ~1 #>
         Thm.generalize (map #1 tfrees, []) 0 #>
         Thm.strip_shyps);
     val local_result =