src/HOL/Tools/Function/function.ML

     val ((goal_state, afterqed), lthy') =
       prepare_function do_print prep default_constraint fixspec eqns config lthy
   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 =
   gen_function false Specification.check_spec default_constraint_any
 fun function_cmd a b c int =