@@ -2157,10 +2157,14 @@ runElabAction ist fc env tm ns = do tm' <- eval tm
2157 datatypes <- get_datatypes
2157 datatypes <- get_datatypes
2158 env <- get_env
2158 env <- get_env
2159 (_, ES (p, aux') _ _) <-
2159 (_, ES (p, aux') _ _) <-
2160+ do (ES (current_p, _) _ _) <- get
2160− lift $ runElab aux (runElabAction ist fc [] script ns)
2161+ lift $ runElab aux (runElabAction ist fc [] script ns)
2161− (newProof recH ctxt datatypes goalTT)
2162+ ((newProof recH ctxt datatypes goalTT)
2163+ { nextname = nextname current_p})
2162 let tm_out = getProofTerm (pterm p)
2164 let tm_out = getProofTerm (pterm p)
2163− updateAux $ const aux'
2165+ do (ES (prf, _) s e) <- get
2166+ let p' = prf { nextname = nextname p }
2167+ put (ES (p', aux') s e)
2164 env' <- get_env
2168 env' <- get_env
2165 (tm, ty, _) <- lift $ recheck ctxt env (forget tm_out) tm_out
2169 (tm, ty, _) <- lift $ recheck ctxt env (forget tm_out) tm_out
2166 let (tm', ty') = (reflect tm, reflect ty)
2170 let (tm', ty') = (reflect tm, reflect ty)