diff --git a/pkgs/applications/science/logic/isabelle/default.nix b/pkgs/applications/science/logic/isabelle/default.nix
index 98b71b7f5007..6c51fb5192d4 100644
--- a/pkgs/applications/science/logic/isabelle/default.nix
+++ b/pkgs/applications/science/logic/isabelle/default.nix
@@ -1,23 +1,23 @@
-{ stdenv, fetchurl, perl, nettools, java, polyml, proofgeneral }:
+{ stdenv, fetchurl, perl, nettools, java, polyml }:
 # nettools needed for hostname
 
 let
-  dirname = "Isabelle2015";
+  dirname = "Isabelle2016";
   theories = ["HOL" "FOL" "ZF"];
 in
 
 stdenv.mkDerivation {
-  name = "isabelle-2015";
+  name = "isabelle-2016";
   inherit dirname theories;
 
   src = if stdenv.isDarwin
     then fetchurl {
-      url = http://isabelle.in.tum.de/dist/Isabelle2015.dmg;
-      sha256 = "1vhm10qc1rn3wy9r12clrl33p64h3q1aj41mcnxkbnsyg2bx03im";
+      url = "http://isabelle.in.tum.de/website-${dirname}/dist/${dirname}.dmg";
+      sha256 = "0wawf0cjc52h8hif1867p33qhlh6qz0fy5i2kr1gbf7psickd6iw";
     }
     else fetchurl {
-      url = http://isabelle.in.tum.de/dist/Isabelle2015_linux.tar.gz;
-      sha256 = "13kqm458d8mw7il1zg5bdb1nfbb869p331d75xzlm2v9xgjxx862";
+      url = "http://isabelle.in.tum.de/website-${dirname}/dist/${dirname}_linux.tar.gz";
+      sha256 = "0jh1qrsyib13fycymwvw7dq7xfy4iyplwq0s65ash842cdzkbxb4";
     };
 
   buildInputs = [ perl polyml ]
@@ -34,17 +34,14 @@ stdenv.mkDerivation {
       --replace /usr/bin/env $ENV
     sed -i 's|isabelle_java java|${java}/bin/java|g' lib/Tools/java
     substituteInPlace etc/settings \
-      --subst-var-by ML_HOME "${polyml}/bin" \
-      --subst-var-by PROOFGENERAL_HOME "${proofgeneral}/share/emacs/site-lisp/ProofGeneral"
+      --subst-var-by ML_HOME "${polyml}/bin"
     substituteInPlace contrib/jdk/etc/settings \
       --replace ISABELLE_JDK_HOME= '#ISABELLE_JDK_HOME='
     substituteInPlace contrib/polyml-*/etc/settings \
-      --replace 'ML_HOME="$POLYML_HOME/$ML_PLATFORM"' \
-                "ML_HOME=\"${polyml}/bin\""
-  '';
-
-  buildPhase = ''
-    ISABELLE_JDK_HOME=${java} ./bin/isabelle build -s $theories
+      --replace '$POLYML_HOME/$ML_PLATFORM' ${polyml}/bin \
+      --replace '$POLYML_HOME/$PLATFORM/polyml' ${polyml}/bin/poly
+    substituteInPlace lib/scripts/run-polyml* lib/scripts/polyml-version \
+      --replace '$ML_HOME/poly' ${polyml}/bin/poly
   '';
 
   installPhase = ''
diff --git a/pkgs/development/compilers/polyml/default.nix b/pkgs/development/compilers/polyml/default.nix
index 276065ad3503..8b5d14e7f5fb 100644
--- a/pkgs/development/compilers/polyml/default.nix
+++ b/pkgs/development/compilers/polyml/default.nix
@@ -1,7 +1,7 @@
 {stdenv, fetchurl, autoreconfHook}:
 
 let
-  version = "5.5.2";
+  version = "5.6";
 in
 
 stdenv.mkDerivation {
@@ -15,7 +15,7 @@ stdenv.mkDerivation {
 
   src = fetchurl {
     url = "mirror://sourceforge/polyml/polyml.${version}.tar.gz";
-    sha256 = "10m680qdad6bd50bav9xjsgmsxw8yxg55vr7grbg0gvykzl2pzbk";
+    sha256 = "05d6l2a5m9jf32a8kahwg2p2ph4x9rjf1nsl83331q3gwn5bkmr0";
   };
 
   meta = {
diff --git a/pkgs/top-level/all-packages.nix b/pkgs/top-level/all-packages.nix
index 424cb2670198..210b74c232fb 100644
--- a/pkgs/top-level/all-packages.nix
+++ b/pkgs/top-level/all-packages.nix
@@ -15384,7 +15384,6 @@ let
   tini = callPackage ../applications/virtualization/tini {};
 
   isabelle = callPackage ../applications/science/logic/isabelle {
-    inherit (pkgs.emacs24Packages) proofgeneral;
     java = if stdenv.isLinux then jre else jdk;
   };