# HG changeset patch
# User blanchet
# Date 1410177781 -7200
# Node ID 2e771e0e50ee1fdbb7b16603401d50537434d64c
# Parent  cd7868fd8f01adbd485bc03f2464ef0e9d543aab
export one more ML function

diff -r cd7868fd8f01 -r 2e771e0e50ee src/HOL/Tools/BNF/bnf_fp_def_sugar.ML
--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Mon Sep 08 14:03:01 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Mon Sep 08 14:03:01 2014 +0200
@@ -81,6 +81,8 @@
     int list list -> term ->
     typ list list
     * (typ list list list list * typ list list list * typ list list list list * typ list)
+  val define_co_rec_as: BNF_Util.fp_kind -> typ -> typ list -> binding -> term -> local_theory ->
+    (term * thm) * local_theory
   val define_rec:
     typ list list * typ list list list list * term list list * term list list list list ->
     (string -> binding) -> typ list -> typ list -> term list -> term -> Proof.context ->
@@ -521,7 +523,7 @@
     Term.lambda c (mk_IfN absT cps ts)
   end;
 
-fun define_co_rec fp fpT Cs b rhs lthy0 =
+fun define_co_rec_as fp fpT Cs b rhs lthy0 =
   let
     val thy = Proof_Context.theory_of lthy0;
 
@@ -546,7 +548,7 @@
     val (ctor_rec_absTs, fpT) = strip_typeN nn (fastype_of ctor_rec)
       |>> map domain_type ||> domain_type;
   in
-    define_co_rec Least_FP fpT Cs (mk_binding recN)
+    define_co_rec_as Least_FP fpT Cs (mk_binding recN)
       (fold_rev (fold_rev Term.lambda) fss (Term.list_comb (ctor_rec,
          map4 (fn ctor_rec_absT => fn rep => fn fs => fn xsss =>
              mk_case_absumprod ctor_rec_absT rep fs (map (map HOLogic.mk_tuple) xsss)
@@ -559,7 +561,7 @@
     val nn = length fpTs;
     val fpT = range_type (snd (strip_typeN nn (fastype_of dtor_corec)));
   in
-    define_co_rec Greatest_FP fpT Cs (mk_binding corecN)
+    define_co_rec_as Greatest_FP fpT Cs (mk_binding corecN)
       (fold_rev (fold_rev Term.lambda) pgss (Term.list_comb (dtor_corec,
          map5 mk_preds_getterss_join cs cpss f_absTs abss cqgsss)))
   end;