diff -r b065b4833092 -r 4d04e14d7ab8 src/HOL/Tools/Function/fun.ML
--- a/src/HOL/Tools/Function/fun.ML	Mon May 30 14:15:44 2016 +0200
+++ b/src/HOL/Tools/Function/fun.ML	Mon May 30 20:58:16 2016 +0200
@@ -174,6 +174,6 @@
   Outer_Syntax.local_theory' @{command_keyword fun}
     "define general recursive functions (short version)"
     (function_parser fun_config
-      >> (fn ((config, fixes), statements) => add_fun_cmd fixes statements config))
+      >> (fn (config, (fixes, specs)) => add_fun_cmd fixes specs config))
 
 end