src/HOL/Tools/Function/function.ML

--- a/src/HOL/Tools/Function/function.ML	Sat Dec 12 15:37:42 2015 +0100
+++ b/src/HOL/Tools/Function/function.ML	Sun Dec 13 21:56:15 2015 +0100
@@ -171,7 +171,7 @@
   in
     lthy'
     |> Proof.theorem NONE (snd oo afterqed) [[(Logic.unprotect (Thm.concl_of goal_state), [])]]
-    |> Proof.refine (Method.primitive_text (K (K goal_state))) |> Seq.hd
+    |> Proof.refine_singleton (Method.primitive_text (K (K goal_state)))
   end
 
 val function =