diff -Nuar ProofGeneral-4.0/contrib/mmm/mmm-mode.el ProofGeneral-4.0-nix/contrib/mmm/mmm-mode.el
--- ProofGeneral-4.0/contrib/mmm/mmm-mode.el	2010-10-11 00:56:57.000000000 +0200
+++ ProofGeneral-4.0-nix/contrib/mmm/mmm-mode.el	2011-05-14 21:55:12.000000000 +0200
@@ -160,9 +160,9 @@
      (mmm-add-hooks)
      (mmm-fixup-skeleton)
      (make-local-variable 'font-lock-fontify-region-function)
-     (make-local-variable 'font-lock-beginning-of-syntax-function)
+     (make-local-variable 'syntax-begin-function)
      (setq font-lock-fontify-region-function 'mmm-fontify-region
-	   font-lock-beginning-of-syntax-function 'mmm-beginning-of-syntax)
+	   syntax-begin-function 'mmm-beginning-of-syntax)
      (setq mmm-mode t)
      (condition-case err
 	 (mmm-apply-all)
@@ -190,7 +190,7 @@
     (mmm-update-submode-region)
     (setq font-lock-fontify-region-function
 	  (get mmm-primary-mode 'mmm-fontify-region-function)
-	  font-lock-beginning-of-syntax-function
+	  syntax-begin-function
 	  (get mmm-primary-mode 'mmm-beginning-of-syntax-function))
     (mmm-update-font-lock-buffer)
     (mmm-refontify-maybe)
diff -Nuar ProofGeneral-4.0/contrib/mmm/mmm-region.el ProofGeneral-4.0-nix/contrib/mmm/mmm-region.el
--- ProofGeneral-4.0/contrib/mmm/mmm-region.el	2010-10-11 00:56:57.000000000 +0200
+++ ProofGeneral-4.0-nix/contrib/mmm/mmm-region.el	2011-05-14 21:58:01.000000000 +0200
@@ -548,7 +548,7 @@
 	    (put mode 'mmm-fontify-region-function
 		 font-lock-fontify-region-function))
 	  (put mode 'mmm-beginning-of-syntax-function
-	       font-lock-beginning-of-syntax-function))
+	       syntax-begin-function))
 	;; Get variables
 	(setq global-vars (mmm-get-locals 'global)
 	      buffer-vars (mmm-get-locals 'buffer)
@@ -768,7 +768,7 @@
   ;; For some reason `font-lock-fontify-block' binds this to nil, thus
   ;; preventing `mmm-beginning-of-syntax' from doing The Right Thing.
   ;; I don't know why it does this, but let's undo it here.
-  (let ((font-lock-beginning-of-syntax-function 'mmm-beginning-of-syntax))
+  (let ((syntax-begin-function 'mmm-beginning-of-syntax))
     (mapc #'(lambda (elt)
 		(when (get (car elt) 'mmm-font-lock-mode)
 		  (mmm-fontify-region-list (car elt) (cdr elt))))