more thorough strip_shyps for proof boxes (but types are usually stripped and reconstructed later);

--- a/src/Pure/thm.ML	Mon Mar 09 14:30:09 2020 +0100
+++ b/src/Pure/thm.ML	Mon Mar 09 15:38:52 2020 +0100
@@ -1065,7 +1065,7 @@
   | thm_deps thm = raise THM ("thm_deps: bad promises", 0, [thm]);
 
 fun name_derivation name_pos =
-  solve_constraints #> (fn thm as Thm (der, args) =>
+  strip_shyps #> (fn thm as Thm (der, args) =>
     let
       val thy = theory_of_thm thm;
 
@@ -1734,7 +1734,7 @@
 
 (*Internalize sort constraints of type variables*)
 val unconstrainT =
-  solve_constraints #> (fn thm as Thm (der, args) =>
+  strip_shyps #> (fn thm as Thm (der, args) =>
     let
       val Deriv {promises, body} = der;
       val {cert, shyps, hyps, tpairs, prop, ...} = args;