proper adjust_maxidx: assms could have maxidx >= 0, e.g. from command "subgoal premises";
--- 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 =