avoid vacous type variable, due to "potentially redundant" shyps in Thm.unconstrainT;
--- a/src/Pure/Thy/export_theory.ML Mon Mar 23 12:29:40 2020 +0100
+++ b/src/Pure/Thy/export_theory.ML Tue Mar 24 13:43:29 2020 +0100
@@ -251,7 +251,7 @@
(* theorems and proof terms *)
val clean_thm = Thm.check_hyps (Context.Theory thy) #> Thm.strip_shyps;
- val prep_thm = clean_thm #> Thm.unconstrainT;
+ val prep_thm = clean_thm #> Thm.unconstrainT #> Thm.strip_shyps;
val lookup_thm_id = Global_Theory.lookup_thm_id thy;