more opportunistic string_of_clause, to make double-sure its Syntax.string_of_term uncheck phase does not crash, and thus bomb ambiguous input via failed composition of warning (e.g. HOL/Imperative_HOL/ex/Linked_List.thy: lemma merge_simps);
;;; Options for Proof General
;;;
;;; Examples for sensible settings:
;; keep sources clean
(custom-set-variables '(indent-tabs-mode nil))
;; retain vital AltGr behaviour, e.g. on non-US Mac OS X
;(custom-set-variables '(ns-alternate-modifier 'none))
;; longer timeout for saving persistent session
;(custom-set-variables '(proof-shell-quit-timeout 60))