X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Ftests%2Fbad_induction.ma;h=99c6b5898b6c0680c9c7d3dea3a302cf66066902;hb=a88be1ca42c0969dbab9a5c76240f5931df876d9;hp=b009e18d15d04aea4302428a440804967931a580;hpb=d16ded65610c520937da64721fa34879f167a943;p=helm.git

diff --git a/helm/software/matita/tests/bad_induction.ma b/helm/software/matita/tests/bad_induction.ma
index b009e18d1..99c6b5898 100644
--- a/helm/software/matita/tests/bad_induction.ma
+++ b/helm/software/matita/tests/bad_induction.ma
@@ -12,7 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-set "baseuri" "cic:/matita/nat/bad_induction".
+
 
 include "nat/nat.ma".
 
@@ -23,5 +23,5 @@ axiom bad_ind : ∀P : nat -> Prop. ∀n.(n = O -> P n) -> (∀n.P n -> P (S n))
 theorem absurd: ∀n. n = O.
   intros.
   letin P ≝ (λx:nat. n = O).
-  apply (bad_ind P n); simplify; intros; autobatch.
+  apply (bad_ind P n); simplify; intros; unfold; autobatch.
 qed.
\ No newline at end of file