X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2FmatitaScript.ml;h=a27b0183197557d16f9782d5099580ef04274391;hb=a7f664e6b4cda35865cb3619800527204a651ba3;hp=ae33d1f83ce4a3d31f391a1ebef36844857c8c07;hpb=cc23f034c9419186602d9250456241f2eba90d7c;p=helm.git

diff --git a/helm/software/matita/matitaScript.ml b/helm/software/matita/matitaScript.ml
index ae33d1f83..a27b01831 100644
--- a/helm/software/matita/matitaScript.ml
+++ b/helm/software/matita/matitaScript.ml
@@ -534,7 +534,7 @@ let rec eval_macro include_paths (buffer : GText.buffer) guistuff lexicon_status
             Auto.revision time size depth
         in
         let proof_script = 
-          if List.exists (fun (s,_) -> s = "paramodulation") params then
+          if List.exists (fun (s,_) -> s = "paramodulation") (snd params) then
               let proof_term, how_many_lambdas = 
                 Auto.lambda_close ~prefix_name:"orrible_hack_" 
                   proof_term menv cc