added convenience function
authorblanchet
Wed, 05 Jun 2013 09:56:28 +0200
changeset 52295 e8a482afb53d
parent 52294 23929f647f79
child 52296 45b5935b11b4
added convenience function
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);