# HG changeset patch
# User wenzelm
# Date 1631216651 -7200
# Node ID 8cff7900871f28c4eebd0fed00eeeba2606bc4ce
# Parent  57b323e2076348d5c9aba682f9c4adc265d0a2cb
tuned;

diff -r 57b323e20763 -r 8cff7900871f src/Pure/Isar/expression.ML
--- 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));