# HG changeset patch
# User wenzelm
# Date 1519140014 -3600
# Node ID b4db2e7e414ec392c279df7b297d571d2bc67564
# Parent  ac4b475fc8c3b251572e251d152c99825c1cadc9
tuned;

diff -r ac4b475fc8c3 -r b4db2e7e414e src/Pure/global_theory.ML
--- a/src/Pure/global_theory.ML	Tue Feb 20 14:03:31 2018 +0100
+++ b/src/Pure/global_theory.ML	Tue Feb 20 16:20:14 2018 +0100
@@ -116,8 +116,8 @@
   |> (if name = "" orelse pre andalso Thm.has_name_hint thm then I
       else Thm.put_name_hint name);
 
-fun name_thms pre official name xs =
-  map (uncurry (name_thm pre official)) (name_multi name xs);
+fun name_thms pre official name thms =
+  map (uncurry (name_thm pre official)) (name_multi name thms);
 
 fun name_thmss official name fact =
   burrow_fact (name_thms true official name) fact;