src/HOL/Tools/primrec_package.ML

   val add_primrec_global: (binding * typ option * mixfix) list ->
     (Attrib.binding * term) list -> theory -> thm list * theory
   val add_primrec_overloaded: (string * (string * typ) * bool) list ->
     (binding * typ option * mixfix) list ->
     (Attrib.binding * term) list -> theory -> thm list * theory
-  val add_primrec_simple: ((binding * typ) * mixfix) list -> (binding * term) list ->
+  val add_primrec_simple: ((binding * typ) * mixfix) list -> term list ->
     local_theory -> (string * thm list list) * local_theory
 end;
 
 structure PrimrecPackage : PRIMREC_PACKAGE =
 struct

       | NONE => ""));
 
 
 (* primrec definition *)
 
-fun add_primrec_simple fixes spec lthy =
-  let
-    val ((prefix, (fs, defs)), prove) = distill lthy fixes (map snd spec);
+fun add_primrec_simple fixes ts lthy =
+  let
+    val ((prefix, (fs, defs)), prove) = distill lthy fixes ts;
   in
     lthy
     |> fold_map (LocalTheory.define Thm.definitionK) defs
     |-> (fn defs => `(fn lthy => (prefix, prove lthy defs)))
   end;

       map (Attrib.internal o K)
         [Simplifier.simp_add, Nitpick_Const_Simp_Thms.add, Quickcheck_RecFun_Simp_Thms.add]);
   in
     lthy
     |> set_group ? LocalTheory.set_group (serial_string ())
-    |> add_primrec_simple fixes spec
+    |> add_primrec_simple fixes (map snd spec)
     |-> (fn (prefix, simps) => fold_map (LocalTheory.note Thm.generatedK)
           (attr_bindings prefix ~~ simps)
     #-> (fn simps' => LocalTheory.note Thm.generatedK
           (simp_attr_binding prefix, maps snd simps')))
     |>> snd