proper grounding of free types produced by reconstruct_proof/infer_type, e.g. relevant for Lattices_Big.semilattice_set.infinite;

--- a/src/Pure/proofterm.ML	Mon Mar 09 16:12:53 2020 +0100
+++ b/src/Pure/proofterm.ML	Mon Mar 09 16:58:23 2020 +0100
@@ -2049,7 +2049,12 @@
   let
     val hidden = hidden_types term proof;
     val idx = Term.maxidx_term term (maxidx_proof proof ~1) + 1;
-    fun smash T = if member (op =) hidden T then TVar (("'", idx), Type.sort_of_atyp T) else T;
+    fun smash T =
+      if member (op =) hidden T then
+        (case Type.sort_of_atyp T of
+          [] => dummyT
+        | S => TVar (("'", idx), S))
+      else T;
     val smashT = map_atyps smash;
   in map_proof_terms (map_types smashT) smashT proof end;