1.1 --- a/src/HOL/Tools/primrec.ML	Wed Feb 17 11:21:59 2010 +0100
     1.2 +++ b/src/HOL/Tools/primrec.ML	Wed Feb 17 13:48:13 2010 +0100
     1.3 @@ -8,16 +8,16 @@
     1.4  signature PRIMREC =
     1.5  sig
     1.6    val add_primrec: (binding * typ option * mixfix) list ->
     1.7 -    (Attrib.binding * term) list -> local_theory -> thm list * local_theory
     1.8 +    (Attrib.binding * term) list -> local_theory -> (term list * thm list) * local_theory
     1.9    val add_primrec_cmd: (binding * string option * mixfix) list ->
    1.10 -    (Attrib.binding * string) list -> local_theory -> thm list * local_theory
    1.11 +    (Attrib.binding * string) list -> local_theory -> (term list * thm list) * local_theory
    1.12    val add_primrec_global: (binding * typ option * mixfix) list ->
    1.13 -    (Attrib.binding * term) list -> theory -> thm list * theory
    1.14 +    (Attrib.binding * term) list -> theory -> (term list * thm list) * theory
    1.15    val add_primrec_overloaded: (string * (string * typ) * bool) list ->
    1.16      (binding * typ option * mixfix) list ->
    1.17 -    (Attrib.binding * term) list -> theory -> thm list * theory
    1.18 +    (Attrib.binding * term) list -> theory -> (term list * thm list) * theory
    1.19    val add_primrec_simple: ((binding * typ) * mixfix) list -> term list ->
    1.20 -    local_theory -> (string * thm list list) * local_theory
    1.21 +    local_theory -> (string * (term list * thm list)) * local_theory
    1.22  end;
    1.23  
    1.24  structure Primrec : PRIMREC =
    1.25 @@ -244,7 +244,7 @@
    1.26          val rewrites = rec_rewrites' @ map (snd o snd) defs;
    1.27          fun tac _ = EVERY [rewrite_goals_tac rewrites, rtac refl 1];
    1.28          val _ = message ("Proving equations for primrec function(s) " ^ commas_quote names);
    1.29 -      in map (fn eq => [Goal.prove lthy frees [] eq tac]) eqs end;
    1.30 +      in map (fn eq => Goal.prove lthy frees [] eq tac) eqs end;
    1.31    in ((prefix, (fs, defs)), prove) end
    1.32    handle PrimrecError (msg, some_eqn) =>
    1.33      error ("Primrec definition error:\n" ^ msg ^ (case some_eqn
    1.34 @@ -260,7 +260,7 @@
    1.35    in
    1.36      lthy
    1.37      |> fold_map Local_Theory.define defs
    1.38 -    |-> (fn defs => `(fn lthy => (prefix, prove lthy defs)))
    1.39 +    |-> (fn defs => `(fn lthy => (prefix, (map fst defs, prove lthy defs))))
    1.40    end;
    1.41  
    1.42  local
    1.43 @@ -285,10 +285,10 @@
    1.44    in
    1.45      lthy
    1.46      |> add_primrec_simple fixes (map snd spec)
    1.47 -    |-> (fn (prefix, simps) => fold_map Local_Theory.note (attr_bindings prefix ~~ simps)
    1.48 +    |-> (fn (prefix, (ts, simps)) => fold_map Local_Theory.note (attr_bindings prefix ~~ map single simps)
    1.49        #-> (fn simps' => Local_Theory.note (simp_attr_binding prefix, maps snd simps')
    1.50 +      #>> (fn (_, simps'') => (ts, simps''))
    1.51        ##> (Spec_Rules.add Spec_Rules.Equational (specs_of simps'))))
    1.52 -    |>> snd
    1.53    end;
    1.54  
    1.55  in
    1.56 @@ -301,16 +301,16 @@
    1.57  fun add_primrec_global fixes specs thy =
    1.58    let
    1.59      val lthy = Theory_Target.init NONE thy;
    1.60 -    val (simps, lthy') = add_primrec fixes specs lthy;
    1.61 +    val ((ts, simps), lthy') = add_primrec fixes specs lthy;
    1.62      val simps' = ProofContext.export lthy' lthy simps;
    1.63 -  in (simps', Local_Theory.exit_global lthy') end;
    1.64 +  in ((ts, simps'), Local_Theory.exit_global lthy') end;
    1.65  
    1.66  fun add_primrec_overloaded ops fixes specs thy =
    1.67    let
    1.68      val lthy = Theory_Target.overloading ops thy;
    1.69 -    val (simps, lthy') = add_primrec fixes specs lthy;
    1.70 +    val ((ts, simps), lthy') = add_primrec fixes specs lthy;
    1.71      val simps' = ProofContext.export lthy' lthy simps;
    1.72 -  in (simps', Local_Theory.exit_global lthy') end;
    1.73 +  in ((ts, simps'), Local_Theory.exit_global lthy') end;
    1.74  
    1.75  
    1.76  (* outer syntax *)

     2.1 --- a/src/HOL/Tools/quickcheck_generators.ML	Wed Feb 17 11:21:59 2010 +0100
     2.2 +++ b/src/HOL/Tools/quickcheck_generators.ML	Wed Feb 17 13:48:13 2010 +0100
     2.3 @@ -139,7 +139,7 @@
     2.4      val eqs0 = [subst_v @{term "0::code_numeral"} eq,
     2.5        subst_v (@{term "Suc_code_numeral"} $ t_k) eq];
     2.6      val eqs1 = map (Pattern.rewrite_term thy rew_ts []) eqs0;
     2.7 -    val ((_, eqs2), lthy') = Primrec.add_primrec_simple
     2.8 +    val ((_, (_, eqs2)), lthy') = Primrec.add_primrec_simple
     2.9        [((Binding.conceal (Binding.name random_aux), T), NoSyn)] eqs1 lthy;
    2.10      val cT_random_aux = inst pt_random_aux;
    2.11      val cT_rhs = inst pt_rhs;
    2.12 @@ -148,7 +148,7 @@
    2.13             [(cT_random_aux, cert t_random_aux), (cT_rhs, cert t_rhs)]);
    2.14      val tac = ALLGOALS (rtac rule)
    2.15        THEN ALLGOALS (simp_tac rew_ss)
    2.16 -      THEN (ALLGOALS (ProofContext.fact_tac (flat eqs2)))
    2.17 +      THEN (ALLGOALS (ProofContext.fact_tac eqs2))
    2.18      val simp = Skip_Proof.prove lthy' [v] [] eq (K tac);
    2.19    in (simp, lthy') end;
    2.20