# HG changeset patch
# User haftmann
# Date 1266410893 -3600
# Node ID a57ef2cd22368a94aa52c05fb940a2c8c756552b
# Parent  58b9503a7f9adc5ee9536c9582adcd16b5f5536f
tuned primrec signature: return definienda

diff -r 58b9503a7f9a -r a57ef2cd2236 src/HOL/Tools/primrec.ML
--- a/src/HOL/Tools/primrec.ML	Wed Feb 17 11:21:59 2010 +0100
+++ b/src/HOL/Tools/primrec.ML	Wed Feb 17 13:48:13 2010 +0100
@@ -8,16 +8,16 @@
 signature PRIMREC =
 sig
   val add_primrec: (binding * typ option * mixfix) list ->
-    (Attrib.binding * term) list -> local_theory -> thm list * local_theory
+    (Attrib.binding * term) list -> local_theory -> (term list * thm list) * local_theory
   val add_primrec_cmd: (binding * string option * mixfix) list ->
-    (Attrib.binding * string) list -> local_theory -> thm list * local_theory
+    (Attrib.binding * string) list -> local_theory -> (term list * thm list) * local_theory
   val add_primrec_global: (binding * typ option * mixfix) list ->
-    (Attrib.binding * term) list -> theory -> thm list * theory
+    (Attrib.binding * term) list -> theory -> (term list * 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
+    (Attrib.binding * term) list -> theory -> (term list * thm list) * theory
   val add_primrec_simple: ((binding * typ) * mixfix) list -> term list ->
-    local_theory -> (string * thm list list) * local_theory
+    local_theory -> (string * (term list * thm list)) * local_theory
 end;
 
 structure Primrec : PRIMREC =
@@ -244,7 +244,7 @@
         val rewrites = rec_rewrites' @ map (snd o snd) defs;
         fun tac _ = EVERY [rewrite_goals_tac rewrites, rtac refl 1];
         val _ = message ("Proving equations for primrec function(s) " ^ commas_quote names);
-      in map (fn eq => [Goal.prove lthy frees [] eq tac]) eqs end;
+      in map (fn eq => Goal.prove lthy frees [] eq tac) eqs end;
   in ((prefix, (fs, defs)), prove) end
   handle PrimrecError (msg, some_eqn) =>
     error ("Primrec definition error:\n" ^ msg ^ (case some_eqn
@@ -260,7 +260,7 @@
   in
     lthy
     |> fold_map Local_Theory.define defs
-    |-> (fn defs => `(fn lthy => (prefix, prove lthy defs)))
+    |-> (fn defs => `(fn lthy => (prefix, (map fst defs, prove lthy defs))))
   end;
 
 local
@@ -285,10 +285,10 @@
   in
     lthy
     |> add_primrec_simple fixes (map snd spec)
-    |-> (fn (prefix, simps) => fold_map Local_Theory.note (attr_bindings prefix ~~ simps)
+    |-> (fn (prefix, (ts, simps)) => fold_map Local_Theory.note (attr_bindings prefix ~~ map single simps)
       #-> (fn simps' => Local_Theory.note (simp_attr_binding prefix, maps snd simps')
+      #>> (fn (_, simps'') => (ts, simps''))
       ##> (Spec_Rules.add Spec_Rules.Equational (specs_of simps'))))
-    |>> snd
   end;
 
 in
@@ -301,16 +301,16 @@
 fun add_primrec_global fixes specs thy =
   let
     val lthy = Theory_Target.init NONE thy;
-    val (simps, lthy') = add_primrec fixes specs lthy;
+    val ((ts, simps), lthy') = add_primrec fixes specs lthy;
     val simps' = ProofContext.export lthy' lthy simps;
-  in (simps', Local_Theory.exit_global lthy') end;
+  in ((ts, simps'), Local_Theory.exit_global lthy') end;
 
 fun add_primrec_overloaded ops fixes specs thy =
   let
     val lthy = Theory_Target.overloading ops thy;
-    val (simps, lthy') = add_primrec fixes specs lthy;
+    val ((ts, simps), lthy') = add_primrec fixes specs lthy;
     val simps' = ProofContext.export lthy' lthy simps;
-  in (simps', Local_Theory.exit_global lthy') end;
+  in ((ts, simps'), Local_Theory.exit_global lthy') end;
 
 
 (* outer syntax *)
diff -r 58b9503a7f9a -r a57ef2cd2236 src/HOL/Tools/quickcheck_generators.ML
--- a/src/HOL/Tools/quickcheck_generators.ML	Wed Feb 17 11:21:59 2010 +0100
+++ b/src/HOL/Tools/quickcheck_generators.ML	Wed Feb 17 13:48:13 2010 +0100
@@ -139,7 +139,7 @@
     val eqs0 = [subst_v @{term "0::code_numeral"} eq,
       subst_v (@{term "Suc_code_numeral"} $ t_k) eq];
     val eqs1 = map (Pattern.rewrite_term thy rew_ts []) eqs0;
-    val ((_, eqs2), lthy') = Primrec.add_primrec_simple
+    val ((_, (_, eqs2)), lthy') = Primrec.add_primrec_simple
       [((Binding.conceal (Binding.name random_aux), T), NoSyn)] eqs1 lthy;
     val cT_random_aux = inst pt_random_aux;
     val cT_rhs = inst pt_rhs;
@@ -148,7 +148,7 @@
            [(cT_random_aux, cert t_random_aux), (cT_rhs, cert t_rhs)]);
     val tac = ALLGOALS (rtac rule)
       THEN ALLGOALS (simp_tac rew_ss)
-      THEN (ALLGOALS (ProofContext.fact_tac (flat eqs2)))
+      THEN (ALLGOALS (ProofContext.fact_tac eqs2))
     val simp = Skip_Proof.prove lthy' [v] [] eq (K tac);
   in (simp, lthy') end;