diff -r c9605a284fba -r 2f18172214c8 src/HOL/HOLCF/Tools/fixrec.ML
--- a/src/HOL/HOLCF/Tools/fixrec.ML	Wed Apr 27 10:03:35 2016 +0200
+++ b/src/HOL/HOLCF/Tools/fixrec.ML	Thu Apr 28 09:43:11 2016 +0200
@@ -334,7 +334,7 @@
     val (skips, raw_spec) = ListPair.unzip raw_spec'
     val (fixes : ((binding * typ) * mixfix) list,
          spec : (Attrib.binding * term) list) =
-          fst (prep_spec raw_fixes raw_spec lthy)
+          fst (prep_spec raw_fixes (map (rpair []) raw_spec) lthy)
     val names = map (Binding.name_of o fst o fst) fixes
     fun check_head name =
         member (op =) names name orelse
@@ -377,8 +377,8 @@
 
 in
 
-val add_fixrec = gen_fixrec Specification.check_spec
-val add_fixrec_cmd = gen_fixrec Specification.read_spec
+val add_fixrec = gen_fixrec Specification.check_multi_specs
+val add_fixrec_cmd = gen_fixrec Specification.read_multi_specs
 
 end (* local *)
 
@@ -394,13 +394,13 @@
 val spec' : (bool * (Attrib.binding * string)) parser =
   opt_thm_name' -- Parse.prop >> (fn ((a, b), c) => (a, (b, c)))
 
-val alt_specs' : (bool * (Attrib.binding * string)) list parser =
+val multi_specs' : (bool * (Attrib.binding * string)) list parser =
   let val unexpected = Scan.ahead (Parse.name || @{keyword "["} || @{keyword "("})
   in Parse.enum1 "|" (spec' --| Scan.option (unexpected -- Parse.!!! @{keyword "|"})) end
 
 val _ =
   Outer_Syntax.local_theory @{command_keyword fixrec} "define recursive functions (HOLCF)"
-    (Parse.fixes -- (Parse.where_ |-- Parse.!!! alt_specs')
+    (Parse.fixes -- (Parse.where_ |-- Parse.!!! multi_specs')
       >> (fn (fixes, specs) => add_fixrec_cmd fixes specs))
 
 end