diff -r a3f565b8ba76 -r 9c94e6a30d29 src/HOL/Tools/Function/termination.ML
--- a/src/HOL/Tools/Function/termination.ML	Mon Jun 01 13:32:36 2015 +0200
+++ b/src/HOL/Tools/Function/termination.ML	Mon Jun 01 13:35:16 2015 +0200
@@ -142,9 +142,9 @@
         Const (@{const_abbrev Set.empty}, fastype_of c1))
       |> HOLogic.mk_Trueprop (* "C1 O C2 = {}" *)
   in
-    case Function_Lib.try_proof (Thm.cterm_of ctxt goal) chain_tac of
+    (case Function_Lib.try_proof ctxt (Thm.cterm_of ctxt goal) chain_tac of
       Function_Lib.Solved thm => SOME thm
-    | _ => NONE
+    | _ => NONE)
   end
 
 
@@ -167,22 +167,22 @@
 fun mk_desc ctxt tac vs Gam l r m1 m2 =
   let
     fun try rel =
-      try_proof (Thm.cterm_of ctxt
+      try_proof ctxt (Thm.cterm_of ctxt
         (Logic.list_all (vs,
            Logic.mk_implies (HOLogic.mk_Trueprop Gam,
-             HOLogic.mk_Trueprop (Const (rel, @{typ "nat => nat => bool"})
+             HOLogic.mk_Trueprop (Const (rel, @{typ "nat \<Rightarrow> nat \<Rightarrow> bool"})
                $ (m2 $ r) $ (m1 $ l)))))) tac
   in
-    case try @{const_name Orderings.less} of
-       Solved thm => Less thm
-     | Stuck thm =>
-       (case try @{const_name Orderings.less_eq} of
+    (case try @{const_name Orderings.less} of
+      Solved thm => Less thm
+    | Stuck thm =>
+        (case try @{const_name Orderings.less_eq} of
           Solved thm2 => LessEq (thm2, thm)
         | Stuck thm2 =>
-          if Thm.prems_of thm2 = [HOLogic.Trueprop $ @{term False}]
-          then False thm2 else None (thm2, thm)
+            if Thm.prems_of thm2 = [HOLogic.Trueprop $ @{term False}]
+            then False thm2 else None (thm2, thm)
         | _ => raise Match) (* FIXME *)
-     | _ => raise Match
+    | _ => raise Match)
 end
 
 fun prove_descent ctxt tac sk (c, (m1, m2)) =