tuned;

--- a/src/Pure/Isar/expression.ML	Thu Sep 09 21:37:42 2021 +0200
+++ b/src/Pure/Isar/expression.ML	Thu Sep 09 21:44:11 2021 +0200
@@ -815,7 +815,7 @@
       |> prep_decl raw_import I raw_body;
     val text as (((_, exts'), _), defs) = eval ctxt' deps body_elems;
 
-    val type_tfrees = TFrees.build (fold TFrees.add_tfreesT (map snd parms));
+    val type_tfrees = TFrees.build (fold (TFrees.add_tfreesT o #2) parms);
     val extra_tfrees =
       TFrees.build (exts' |> (fold o Term.fold_types o Term.fold_atyps)
         (fn TFree v => not (TFrees.defined type_tfrees v) ? TFrees.add_set v | _ => I));