diff -r 2618e7e3b5ea -r e966c311e9a7 src/HOL/Tools/Function/function_common.ML
--- a/src/HOL/Tools/Function/function_common.ML	Fri Sep 04 11:38:35 2015 +0200
+++ b/src/HOL/Tools/Function/function_common.ML	Fri Sep 04 13:39:20 2015 +0200
@@ -282,7 +282,7 @@
 
 fun termination_rule_tac ctxt = resolve_tac ctxt (#1 (Data.get (Context.Proof ctxt)))
 
-val store_termination_rule = Data.map o @{apply 4(1)} o cons
+val store_termination_rule = Data.map o @{apply 4(1)} o cons o Thm.trim_context
 
 val get_functions = #2 o Data.get o Context.Proof
 fun add_function_data (info : info as {fs, termination, ...}) =