src/HOL/BNF/Tools/bnf_fp_rec_sugar.ML

 
 signature BNF_FP_REC_SUGAR =
 sig
   val add_primrec_cmd: (binding * string option * mixfix) list ->
     (Attrib.binding * string) list -> local_theory -> local_theory;
+  val add_primcorec_cmd: bool ->
+    (binding * string option * mixfix) list * (Attrib.binding * string) list -> Proof.context ->
+    Proof.state
 end;
 
 (* TODO:
      - error handling for indirect calls
 *)

 
 fun finds eq = fold_map (fn x => List.partition (curry eq x) #>> pair x);
 
 val simp_attrs = @{attributes [simp]};
 
+
+
+(* Primrec *)
 
 type eqn_data = {
   fun_name: string,
   rec_type: typ,
   ctr: term,

     then error ("primrec_new error:\n  " ^ str)
     else error ("primrec_new error:\n  " ^ str ^ "\nin\n  " ^
       space_implode "\n  " (map (quote o Syntax.string_of_term lthy) eqns))
 
 
-val _ = Outer_Syntax.local_theory
-  @{command_spec "primrec_new"}
-  "define primitive recursive functions"
-  (Parse.fixes -- Parse_Spec.where_alt_specs >> uncurry add_primrec_cmd);
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
+
+(* Primcorec *)
 
 type co_eqn_data_dtr_disc = {
   fun_name: string,
   ctr_no: int,
   cond: term,

     if null eqns
     then error ("primcorec error:\n  " ^ str)
     else error ("primcorec error:\n  " ^ str ^ "\nin\n  " ^
       space_implode "\n  " (map (quote o Syntax.string_of_term lthy) eqns))
 
-val _ = Outer_Syntax.local_theory_to_proof
-  @{command_spec "primcorec"}
-  "define primitive corecursive functions"
-  (Parse.opt_keyword "sequential" -- (Parse.fixes -- Parse_Spec.where_alt_specs) >>
-    uncurry add_primcorec_cmd);
-
 end;