--- a/src/HOL/Library/Code_Lazy.thy Sun May 16 23:22:03 2021 +0200
+++ b/src/HOL/Library/Code_Lazy.thy Mon May 17 13:37:47 2021 +0200
@@ -182,7 +182,7 @@
\<open>object Lazy {
final class Lazy[A] (f: Unit => A) {
var evaluated = false;
- lazy val x: A = f ()
+ lazy val x: A = f(())
def get() : A = {
evaluated = true;
@@ -210,7 +210,7 @@
x: Lazy[A],
dummy: Term) : Term = {
if (x.evaluated)
- app(const("Code_Lazy.delay")(funT(funT(unitT)(ty))(lazyT(ty))))(abs("_")(unitT)(term_of(x.get)))
+ app(const("Code_Lazy.delay")(funT(funT(unitT)(ty))(lazyT(ty))))(abs("_")(unitT)(term_of(x.get())))
else
app(const("Code_Lazy.delay")(funT(funT(unitT)(ty))(lazyT(ty))))(const("Pure.dummy_pattern")(funT(unitT)(ty)))
}