@@ -620,19 +620,19 @@ introTy ty n ctxt env _ = fail "Can't introduce here."
620620
621621intro :: Maybe Name -> RunTactic
622622intro mn ctxt env (Bind x (Hole t) (P _ x' _)) | x == x' =
623− do let n = case mn of
624− Just name -> name
625− Nothing -> x
626− let t' = case t of
623+ do let t' = case t of
627624 x@(Bind y (Pi _ s _) _) -> x
628625 _ -> hnf ctxt env t
629626 case t' of
630627 Bind y (Pi _ s _) t ->
628+ let n = case mn of
629+ Just name -> name
630+ Nothing -> y
631631 -- It's important that this be subst and not updsubst,
632632 -- because we want to substitute even in portions of
633633 -- terms that we know do not contain holes.
634− let t' = subst y (P Bound n s) t in
635− return $ Bind n (Lam s) (Bind x (Hole t') (P Bound x t'))
634+ t' = subst y (P Bound n s) t
635+ in return $ Bind n (Lam s) (Bind x (Hole t') (P Bound x t'))
636636 _ -> lift $ tfail $ CantIntroduce t'
637637intro n ctxt env _ = fail "Can't introduce here."
638638