# HG changeset patch
# User blanchet
# Date 1370418988 -7200
# Node ID e8a482afb53d679155743208d6a76a4a871163ca
# Parent  23929f647f798bd6fe0d2545b12e14b35ed812e1
added convenience function

diff -r 23929f647f79 -r e8a482afb53d src/HOL/BNF/Tools/bnf_fp_def_sugar.ML
--- a/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Wed Jun 05 09:24:16 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Wed Jun 05 09:56:28 2013 +0200
@@ -24,6 +24,7 @@
      un_fold_thmss: thm list list,
      co_rec_thmss: thm list list};
 
+  val of_fp_sugar: (fp_sugar -> 'a list) -> fp_sugar -> 'a
   val morph_fp_sugar: morphism -> fp_sugar -> fp_sugar
   val fp_sugar_of: Proof.context -> string -> fp_sugar option
 
@@ -117,6 +118,8 @@
    un_fold_thmss: thm list list,
    co_rec_thmss: thm list list};
 
+fun of_fp_sugar f (fp_sugar as {index, ...}) = nth (f fp_sugar) index;
+
 fun eq_fp_sugar ({T = T1, fp = fp1, index = index1, fp_res = fp_res1, ...} : fp_sugar,
     {T = T2, fp = fp2, index = index2, fp_res = fp_res2, ...} : fp_sugar) =
   T1 = T2 andalso fp1 = fp2 andalso index1 = index2 andalso eq_fp_result (fp_res1, fp_res2);