# HG changeset patch
# User wenzelm
# Date 1585053809 -3600
# Node ID 4269db8981b8d09dbfb1382858787e80908a555d
# Parent  7fe1a344404a9f7e6e4cdef584338c6d9849812c
avoid vacous type variable, due to "potentially redundant" shyps in Thm.unconstrainT;

diff -r 7fe1a344404a -r 4269db8981b8 src/Pure/Thy/export_theory.ML
--- 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;