X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FgTopLevel%2FgTopLevel.ml;h=de725228e5061096b489880502f1b2ccd2e3ea14;hb=66314ee777ff9215dd45eb0894428537f765fc69;hp=f7d502066fddc2e9f356b0c77c9e181192fe4f4f;hpb=18bd1d094e9227822ea8c0fa4f9668cd8752236f;p=helm.git

diff --git a/helm/gTopLevel/gTopLevel.ml b/helm/gTopLevel/gTopLevel.ml
index f7d502066..de725228e 100644
--- a/helm/gTopLevel/gTopLevel.ml
+++ b/helm/gTopLevel/gTopLevel.ml
@@ -451,7 +451,7 @@ let qed () =
 		  Cic.Constant (UriManager.name_of_uri uri,Some bo,ty,[],[]) 
                 in
 		let (acic,ids_to_inner_types,ids_to_inner_sorts) =
-		  (rendering_window ())#output#load_proof uri proof
+		  (rendering_window ())#output#load_proof proof
 		in
 		  !qed_set_sensitive false ;
 		  (* let's save the theorem and register it to the getter *) 
@@ -564,7 +564,7 @@ let refresh_proof (output : TermViewer.proof_viewer) =
         (uri,
          Cic.CurrentProof (UriManager.name_of_uri uri,metasenv,bo,ty,[],[]))
   in
-   ignore (output#load_proof uri currentproof)
+   ignore (output#load_proof currentproof)
  with
   e ->
  match ProofEngine.get_proof () with
@@ -864,7 +864,7 @@ let
     try
       let mml,(_,(ids_to_terms,ids_to_father_ids,ids_to_conjectures,
           ids_to_hypotheses,_,_)) =
-       ApplyTransformation.mml_of_cic_object uri obj 
+       ApplyTransformation.mml_of_cic_object obj 
       in
        window#set_title (UriManager.string_of_uri uri) ;
        window#misc#hide () ; window#show () ;