diff -r 241cfa881788 -r 5833b556b3b5 src/HOL/Library/Code_Lazy.thy --- 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 @@ \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))) }