--- a/src/Pure/Thy/export_theory.scala Fri Jun 18 14:35:48 2021 +0200
+++ b/src/Pure/Thy/export_theory.scala Fri Jun 18 15:03:12 2021 +0200
@@ -94,7 +94,7 @@
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)),
@@ -236,8 +236,8 @@
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] =
@@ -266,9 +266,9 @@
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)
}
@@ -345,7 +345,7 @@
Thm(
entity.cache(cache),
prop.cache(cache),
- deps.map(cache.string _),
+ deps.map(cache.string),
cache.proof(proof))
}
@@ -558,7 +558,7 @@
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))
}
@@ -738,7 +738,7 @@
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] =