aboutsummaryrefslogtreecommitdiffhomepage
path: root/hol-light
diff options
context:
space:
mode:
Diffstat (limited to 'hol-light')
-rw-r--r--hol-light/hol-light.el2
1 files changed, 1 insertions, 1 deletions
diff --git a/hol-light/hol-light.el b/hol-light/hol-light.el
index f3c983b0..3201e2ff 100644
--- a/hol-light/hol-light.el
+++ b/hol-light/hol-light.el
@@ -400,7 +400,7 @@ the currently open proof.")
proof-tree-find-begin-of-unfinished-proof
'hol-light-find-begin-of-unfinished-proof
;; These ones belong in shell mode
- proof-tree-proof-finished-regexp "No subgoals"
+ proof-tree-branch-finished-regexp "No subgoals"
proof-tree-show-sequent-command
(lambda (id) (format "print_xgoal_of_id \"%s\";;" id))