X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2FmatitaProof.ml;h=99214e724d85cbd061f927e3c9f9f303ebaed866;hb=fdd8107cc53f5e862004aa5fcd48593ee5634234;hp=9afb90a714b36ca53090f0e63b68aa743d2bd9f0;hpb=7deafec4fd4b2eebf4d4061f21ee5c47bd15b062;p=helm.git

diff --git a/helm/matita/matitaProof.ml b/helm/matita/matitaProof.ml
index 9afb90a71..99214e724 100644
--- a/helm/matita/matitaProof.ml
+++ b/helm/matita/matitaProof.ml
@@ -151,7 +151,5 @@ let proof ?uri ~metasenv ~typ () =
   new proof ~typ ~metasenv ~body ?uri ()
 
 let currentProof () = new currentProof
-let instance =
-  let currentProof = lazy (currentProof ()) in 
-  fun () -> Lazy.force currentProof
+let instance = MatitaMisc.singleton currentProof