Remove isar-markup-ml from here

1 files changed, 0 insertions, 8 deletions

diff --git a/isa/isabelle-system.el b/isa/isabelle-system.el
index 2ac5850d..78222588 100644
--- a/isa/isabelle-system.el
+++ b/isa/isabelle-system.el
@@ -262,14 +262,6 @@ until Proof General is restarted."
   :type 'integer
   :setting "print_depth %i;")
 
-;; FIXME: move this somewhere sensible.
-;; (actually only needs setting for isar)
-(setq proof-assistant-setting-format 'isar-markup-ml)
-
-(defun isar-markup-ml (string)
-  "Return marked up version of STRING for Isar if we seem to be using Isar."
-  (if isa-running-isar (format "ML_command {* %s *};" string) string))
-
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 ;;
 ;; Generic Isabelle menu for Isabelle and Isabelle/Isar