src/HOL/Tools/primrec.ML

 *)
 
 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 =
 struct
 

         val frees = (fold o Term.fold_aterms) (fn Free (x, _) =>
           if Variable.is_fixed lthy x then I else insert (op =) x | _ => I) eqs [];
         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
      of SOME eqn => "\nin\n" ^ quote (Syntax.string_of_term lthy eqn)
       | NONE => ""));

   let
     val ((prefix, (fs, defs)), prove) = distill lthy fixes ts;
   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
 
 fun specs_of simps =

       (Binding.qualify true prefix (Binding.name "simps"),
         map (Attrib.internal o K) [Simplifier.simp_add, Nitpick_Simps.add]);
   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
 
 val add_primrec = gen_primrec Specification.check_spec;

 end;
 
 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 *)
 
 local structure P = OuterParse and K = OuterKeyword in