proper adjust_maxidx: assms could have maxidx >= 0, e.g. from command "subgoal premises";
authorwenzelm
Fri, 27 Jul 2018 17:32:16 +0200
changeset 68693 a9bef20b1e47
parent 68692 0c568ec56f37
child 68694 03e104be99af
proper adjust_maxidx: assms could have maxidx >= 0, e.g. from command "subgoal premises";
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 =