src/Pure/Thy/export_theory.scala

       locales.iterator.map(_.entity) ++
       locale_dependencies.iterator.map(_.entity)
 
     def cache(cache: Term.Cache): Theory =
       Theory(cache.string(name),
-        parents.map(cache.string(_)),
+        parents.map(cache.string),
         types.map(_.cache(cache)),
         consts.map(_.cache(cache)),
         axioms.map(_.cache(cache)),
         thms.map(_.cache(cache)),
         classes.map(_.cache(cache)),

     entity: Entity, syntax: Syntax, args: List[String], abbrev: Option[Term.Typ])
   {
     def cache(cache: Term.Cache): Type =
       Type(entity.cache(cache),
         syntax,
-        args.map(cache.string(_)),
-        abbrev.map(cache.typ(_)))
+        args.map(cache.string),
+        abbrev.map(cache.typ))
   }
 
   def read_types(provider: Export.Provider): List[Type] =
     provider.uncompressed_yxml(Export.THEORY_PREFIX + "types").map((tree: XML.Tree) =>
       {

     propositional: Boolean)
   {
     def cache(cache: Term.Cache): Const =
       Const(entity.cache(cache),
         syntax,
-        typargs.map(cache.string(_)),
+        typargs.map(cache.string),
         cache.typ(typ),
-        abbrev.map(cache.term(_)),
+        abbrev.map(cache.term),
         propositional)
   }
 
   def read_consts(provider: Export.Provider): List[Const] =
     provider.uncompressed_yxml(Export.THEORY_PREFIX + "consts").map((tree: XML.Tree) =>

   {
     def cache(cache: Term.Cache): Thm =
       Thm(
         entity.cache(cache),
         prop.cache(cache),
-        deps.map(cache.string _),
+        deps.map(cache.string),
         cache.proof(proof))
   }
 
   def read_thms(provider: Export.Provider): List[Thm] =
     provider.uncompressed_yxml(Export.THEORY_PREFIX + "thms").map((tree: XML.Tree) =>

   }
 
   sealed case class Arity(type_name: String, domain: List[Term.Sort], codomain: String, prop: Prop)
   {
     def cache(cache: Term.Cache): Arity =
-      Arity(cache.string(type_name), domain.map(cache.sort(_)), cache.string(codomain),
+      Arity(cache.string(type_name), domain.map(cache.sort), cache.string(codomain),
         prop.cache(cache))
   }
 
   def read_arities(provider: Export.Provider): List[Arity] =
   {

         cache.string(name),
         rough_classification.cache(cache),
         typargs.map({ case (name, sort) => (cache.string(name), cache.sort(sort)) }),
         args.map({ case (name, typ) => (cache.string(name), cache.typ(typ)) }),
         terms.map({ case (term, typ) => (cache.term(term), cache.typ(typ)) }),
-        rules.map(cache.term(_)))
+        rules.map(cache.term))
   }
 
   def read_spec_rules(provider: Export.Provider): List[Spec_Rule] =
   {
     val body = provider.uncompressed_yxml(Export.THEORY_PREFIX + "spec_rules")