# HG changeset patch
# User haftmann
# Date 1243455066 -7200
# Node ID dcbe1f9fe2cd460de463cb27ee684e57eec11fea
# Parent  3ced22320ceb242f84776be4405a628a3855c786
tuned signature of add_primrec_simple

diff -r 3ced22320ceb -r dcbe1f9fe2cd src/HOL/Tools/primrec_package.ML
--- a/src/HOL/Tools/primrec_package.ML	Wed May 27 22:11:06 2009 +0200
+++ b/src/HOL/Tools/primrec_package.ML	Wed May 27 22:11:06 2009 +0200
@@ -16,7 +16,7 @@
   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;
 
@@ -252,9 +252,9 @@
 
 (* primrec definition *)
 
-fun add_primrec_simple fixes spec lthy =
+fun add_primrec_simple fixes ts lthy =
   let
-    val ((prefix, (fs, defs)), prove) = distill lthy fixes (map snd spec);
+    val ((prefix, (fs, defs)), prove) = distill lthy fixes ts;
   in
     lthy
     |> fold_map (LocalTheory.define Thm.definitionK) defs
@@ -274,7 +274,7 @@
   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