diff -r bcccad156236 -r e9f73d87d904 src/HOL/Tools/Function/termination.ML
--- a/src/HOL/Tools/Function/termination.ML	Wed Apr 08 16:24:22 2015 +0200
+++ b/src/HOL/Tools/Function/termination.ML	Wed Apr 08 19:39:08 2015 +0200
@@ -32,8 +32,6 @@
   val decompose_tac : Proof.context -> ttac
 end
 
-
-
 structure Termination : TERMINATION =
 struct
 
@@ -275,14 +273,13 @@
 
 fun wf_union_tac ctxt st = SUBGOAL (fn _ =>
   let
-    val thy = Proof_Context.theory_of ctxt
     val ((_ $ (_ $ rel)) :: ineqs) = Thm.prems_of st
 
     fun mk_compr ineq =
       let
         val (vars, prems, lhs, rhs) = dest_term ineq
       in
-        mk_pair_compr (fastype_of lhs, vars, lhs, rhs, map (Object_Logic.atomize_term thy) prems)
+        mk_pair_compr (fastype_of lhs, vars, lhs, rhs, map (Object_Logic.atomize_term ctxt) prems)
       end
 
     val relation =
@@ -360,5 +357,4 @@
     else solve_trivial_tac D i
   end)
 
-
 end