aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
-rw-r--r--isa/isa.el2
-rw-r--r--isar/isar.el2
2 files changed, 2 insertions, 2 deletions
diff --git a/isa/isa.el b/isa/isa.el
index 6c4b6315..4b1a1580 100644
--- a/isa/isa.el
+++ b/isa/isa.el
@@ -160,7 +160,7 @@ and script mode."
proof-shell-prompt-pattern "^2?[ML-=#>]>? \372?"
;; for issuing command, not used to track cwd in any way.
- proof-shell-cd-cmd "Library.cd \"%s\";"
+ proof-shell-cd-cmd "ThyLoad.add_path \"%s\";"
;; Escapes for filenames inside ML strings.
;; We also make a hack for Isabelle, by switching from backslashes
diff --git a/isar/isar.el b/isar/isar.el
index de19ab3b..a5a83bf0 100644
--- a/isar/isar.el
+++ b/isar/isar.el
@@ -196,7 +196,7 @@
proof-shell-prompt-pattern "^\\w*[>#] "
;; for issuing command, not used to track cwd in any way.
- proof-shell-cd-cmd "ML_command {* Library.cd \"%s\" *}"
+ proof-shell-cd-cmd "ML_command {* ThyLoad.add_path \"%s\" *}"
;; Escapes for filenames inside ML strings.
;; We also make a hack for a bug in Isabelle, by switching from