# HG changeset patch
# User wenzelm
# Date 1583769503 -3600
# Node ID d7175626d61e8027e66506a7de10c06b4100c8aa
# Parent  82fbfccca7dd0d63836b1608d8974285c26012dd
proper grounding of free types produced by reconstruct_proof/infer_type, e.g. relevant for Lattices_Big.semilattice_set.infinite;

diff -r 82fbfccca7dd -r d7175626d61e src/Pure/proofterm.ML
--- 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;