diff --git a/tools/vim/README.md b/tools/vim/README.md
index 23fe341af6..a105f164b6 100644
--- a/tools/vim/README.md
+++ b/tools/vim/README.md
@@ -80,7 +80,7 @@ Command  | Description
 `hL`     | Send region to be split into words and each word `load`ed.
 `hl`     | Same as above, but also send the region as a command afterwards.
 `hg`     | Send region (should be a quotation) to `g`, to start a new proof.
-`hG`     | Send region to g after quoting it, to start a new proof.
+`hG`     | Send region to `new_goalstack` after quoting it, to start a new proof. Any trailing `Proof[...]` modifiers are passed to HOL too.
 `he`     | Send region (should be a tactic) to `e`, to expand a tactic.
 `hS`     | Send region (should be a quotation) as a new subgoal.
 `hF`     | Send region (should be a quotation) to be proved sufficient then proved.
@@ -103,7 +103,7 @@ Command     | Description
 `hc`        | Interrupt execution (of whichever of the things sent is running).
 `ht`        | Select a quotation, including the  `` ` `` delimiters. Find `` ` `` left of (or under) cursor and select to next `` ` ``.  Also works for Unicode single quotes (`‘` and `’`).
 `hT`        | Select a term: same as above, but with ``` `` ``` delimiters. (Or Unicode `“` and `”`.)
-`ha`        | Select the previous (or if within current) Theorem or Trivialty statement.
+`ha`        | Select the previous (or if within current) `Theorem` or `Triviality` statement, including its `Proof` keyword and associated modifiers.
 `hh`        | A normal h (usually means move cursor left). This one works in both normal and visual modes.
 `hy`        | Toggle HOL's show types trace.
 `hn`        | Toggle HOL's `PP.avoid_unicode` trace.
diff --git a/tools/vim/hol.src b/tools/vim/hol.src
index 8efc73d998..a887a406a0 100644
--- a/tools/vim/hol.src
+++ b/tools/vim/hol.src
@@ -111,8 +111,15 @@ fu! HOLGoal()
 endf
 
 fu! HOLUQGoal()
-  silent keepjumps normal pG$a`)
-  silent keepjumps normal gg0iproofManagerLib.g(`
+  silent keepjumps normal pG
+  if search('^Proof','cbW')
+    silent keepjumps normal I``) (BasicProvers.mk_tacmod "
+    silent keepjumps normal VGJ
+    silent keepjumps normal A") I
+  else
+    silent keepjumps normal GA``) (BasicProvers.mk_tacmod "Proof") I
+  endif
+  silent keepjumps normal gg0iproofManagerLib.new_goalstack([],``
 endf
 
 let s:stripStart     = ')\|\]\|\['
@@ -129,8 +136,8 @@ fu! HOLExpand()
   while search('\%(\%('.s:stripBoth.'\|'.s:stripEnd.'\)\|'.s:delim.'\zs\%('.s:stripBothWords.'\)\)\_s*\%$','cW')
     silent keepjumps normal vG$"_dgg0
   endw
-  keepjumps normal iproofManagerLib.expand(
-  keepjumps normal G$a)
+  keepjumps normal iproofManagerLib.expand(fn HOLgoal => (
+  keepjumps normal G$a) HOLgoal)
 endf
 
 fu! HOLSubgoal()
@@ -197,6 +204,7 @@ fu! HOLSelect(l,r)
     return
   endif
   call search(a:r,"ce")
+  normal zv
 endf
 
 fu! HOLPattern()
@@ -244,7 +252,7 @@ nn <buffer><silent> <LocalLeader>r :call HOLCall(function("HOLF"),["proofManager
 nn <buffer><silent> <LocalLeader>c :call HOLINT()<CR>
 nn <buffer><silent> <LocalLeader>t :call HOLSelect('`\\|‘','`\\|’')<CR>
 nn <buffer><silent> <LocalLeader>T :call HOLSelect('``\\|“','``\\|”')<CR>
-nn <buffer><silent> <LocalLeader>a :call HOLSelect('^Triviality\\|^Theorem','^Proof')<CR>-Vo+
+nn <buffer><silent> <LocalLeader>a :call HOLSelect('^Triviality\\|^Theorem','^Proof$\\|^Proof\[\_.\{-}\]')<CR>Vo+
 nn <buffer><silent> <LocalLeader>y :call HOLCall(function("HOLF"),["Globals.show_types:=not(!Globals.show_types)"])<CR>
 nn <buffer><silent> <LocalLeader>n :call HOLCall(function("HOLF"),["Feedback.set_trace \"PP.avoid_unicode\" (1 - Feedback.current_trace \"PP.avoid_unicode\")"])<CR>
 no <buffer><LocalLeader>h h