
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 @@
 \<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)))
   }




