diff --git a/src/main/isabelle/stateful_ops.ML b/src/main/isabelle/stateful_ops.ML
index 2289e3e6e6311b9fa35d819db29794b433c897a9..18f0d6400b16879fb6b9d68433d0099eb52bb0eb 100644
--- a/src/main/isabelle/stateful_ops.ML
+++ b/src/main/isabelle/stateful_ops.ML
@@ -486,10 +486,10 @@ fun lookup_datatype (name, raw_constructors) =
         (Codec.Left ("unknown datatype " ^ name), lthy)
     | SOME {ctrs, discs, selss, split, split_asm, case_thms, ...} =>
         let
-          val raw_constructors = sort_wrt snd (raw_constructors)
+          val raw_constructors = sort_by snd (raw_constructors)
           val (names, terms) =
             map (fst o dest_Const) ctrs ~~ (discs ~~ selss)
-            |> sort_wrt fst
+            |> sort_by fst
             |> split_list
           fun process (internal_name, name) (disc, sels) =
             (internal_name, (Const (name, dummyT), dummify_types disc, map dummify_types sels))
diff --git a/src/main/isabelle/tactics.ML b/src/main/isabelle/tactics.ML
index 639c1348b43666f15ee9d5dca347ddd16b6f5a77..d2a5ce83b8499bcc45bd0037a992e56f9f7d30c7 100644
--- a/src/main/isabelle/tactics.ML
+++ b/src/main/isabelle/tactics.ML
@@ -31,8 +31,8 @@ fun equiv_tac rule ctxt =
           |> Syntax.check_term ctxt
           |> Thm.cterm_of ctxt
 
-        val insts = [(Thm.cterm_of ctxt p, p_inst)]
-        val rule = Drule.cterm_instantiate insts rule
+        val insts = [(fst (dest_Var p), p_inst)]
+        val rule = Drule.infer_instantiate ctxt insts rule
       in ext_tac (length args) n THEN resolve_tac ctxt [rule] n end)
 
     val maybe_induct =
@@ -53,8 +53,7 @@ fun method_tac pos src = Subgoal.FOCUS (fn {context = ctxt, concl, ...} =>
       |> Scan.catch scan
     val state =
       Proof.theorem NONE (K I) [[(Thm.term_of concl, [])]] ctxt
-      |> Proof.refine m
-      |> Seq.hd
+      |> Proof.refine_singleton m
     val {goal, ...} = Proof.simple_goal state
   in
     HEADGOAL (resolve_tac ctxt [Goal.conclude goal])
@@ -64,4 +63,4 @@ fun pat_completeness_auto_tac ctxt =
   Pat_Completeness.pat_completeness_tac ctxt 1 THEN auto_tac ctxt
 
 fun termination_tac ctxt =
-  Function_Common.termination_prover_tac ctxt
\ No newline at end of file
+  Function_Common.termination_prover_tac true ctxt
\ No newline at end of file
diff --git a/src/main/isabelle/util.ML b/src/main/isabelle/util.ML
index 2401cfb4bd8bcacc8120b11e71e5989f244b7e3e..55be31d116b0e3be15c4ffb19b30b38946213996 100644
--- a/src/main/isabelle/util.ML
+++ b/src/main/isabelle/util.ML
@@ -117,7 +117,7 @@ fun fold_opt _ [] y = SOME y
   | fold_opt f (x :: xs) y = Option.mapPartial (fold_opt f xs) (f x y)
 
 fun fold_res _ [] y = Exn.Res y
-  | fold_res f (x :: xs) y = Exn.maps_result (fold_res f xs) (f x y)
+  | fold_res f (x :: xs) y = Exn.maps_res (fold_res f xs) (f x y)
 
 fun map_generalized f t =
   case t of
@@ -229,7 +229,7 @@ fun homogenize_spec_types ctxt thms =
     val typ = Sign.the_const_type (Proof_Context.theory_of ctxt) head
 
     fun mk_subst (iname, (sort, inst)) =
-      (Thm.ctyp_of ctxt (TVar (iname, sort)), Thm.ctyp_of ctxt inst)
+      ((iname, sort), Thm.ctyp_of ctxt inst)
 
     fun instantiate ((_, ttyp), thm) =
       let
diff --git a/src/main/scala/leon/solvers/isabelle/package.scala b/src/main/scala/leon/solvers/isabelle/package.scala
index c06f4f59b9f1d3eb11bf924d1812c8eb1e30dc8b..2e5341013311cd469c4fb9f1a8d3dabc10ac738d 100644
--- a/src/main/scala/leon/solvers/isabelle/package.scala
+++ b/src/main/scala/leon/solvers/isabelle/package.scala
@@ -22,7 +22,7 @@ import shapeless.tag
 object `package` {
 
   val theory = "Leon_Runtime"
-  val isabelleVersion = "2015"
+  val isabelleVersion = "2016"
 
 
   implicit class FutureResultOps[A](val future: Future[ProverResult[A]]) extends AnyVal {