# HG changeset patch
# User wenzelm
# Date 1461885704 -7200
# Node ID f009347b9072b60ffd2162ed914970e6ee7dbb37
# Parent  8b9401bfd9fd77eb38aee99491db01afe61d0156
re-tuned c9605a284fba, which impacts performance significantly (for unclear reasons) -- make AFP/Collections build again;

diff -r 8b9401bfd9fd -r f009347b9072 src/Pure/Isar/specification.ML
--- a/src/Pure/Isar/specification.ML	Thu Apr 28 15:42:52 2016 +0200
+++ b/src/Pure/Isar/specification.ML	Fri Apr 29 01:21:44 2016 +0200
@@ -101,14 +101,16 @@
 local
 
 fun close_forms ctxt auto_close i prems concls =
-  let
-    val xs =
-      if auto_close then rev (fold (Variable.add_free_names ctxt) (prems @ concls) [])
-      else [];
-    val types =
-      map (Type_Infer.param i o rpair []) (Name.invent Name.context Name.aT (length xs));
-    val uniform_typing = AList.lookup (op =) (xs ~~ types);
-  in map (Logic.close_prop_constraint uniform_typing (xs ~~ xs) prems) concls end;
+  if not auto_close andalso null prems then concls
+  else
+    let
+      val xs =
+        if auto_close then rev (fold (Variable.add_free_names ctxt) (prems @ concls) [])
+        else [];
+      val types =
+        map (Type_Infer.param i o rpair []) (Name.invent Name.context Name.aT (length xs));
+      val uniform_typing = AList.lookup (op =) (xs ~~ types);
+    in map (Logic.close_prop_constraint uniform_typing (xs ~~ xs) prems) concls end;
 
 fun get_positions ctxt x =
   let