From b9c7739fed07fc1b649718046f0d2e491a1bd81e Mon Sep 17 00:00:00 2001
From: David Aspinall
Date: Mon, 29 May 2000 18:33:39 +0000
Subject: Remove isar-markup-ml from here

---
 isa/isabelle-system.el | 8 --------
 1 file changed, 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
-- 
cgit v1.2.3