src/HOL/BNF/Tools/bnf_fp_def_sugar.ML
changeset 53907 d177eb989c65
parent 53901 3d93e8b4ae02
child 53974 612505263257
     1.1 --- a/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Thu Sep 26 09:58:36 2013 +0200
     1.2 +++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Thu Sep 26 10:00:07 2013 +0200
     1.3 @@ -27,6 +27,7 @@
     1.4    val of_fp_sugar: (fp_sugar -> 'a list) -> fp_sugar -> 'a
     1.5    val morph_fp_sugar: morphism -> fp_sugar -> fp_sugar
     1.6    val fp_sugar_of: Proof.context -> string -> fp_sugar option
     1.7 +  val fp_sugars_of: Proof.context -> fp_sugar list
     1.8  
     1.9    val co_induct_of: 'a list -> 'a
    1.10    val strong_co_induct_of: 'a list -> 'a
    1.11 @@ -150,6 +151,9 @@
    1.12     disc_co_itersss = map (map (map (Morphism.thm phi))) disc_co_itersss,
    1.13     sel_co_iterssss = map (map (map (map (Morphism.thm phi)))) sel_co_iterssss};
    1.14  
    1.15 +val transfer_fp_sugar =
    1.16 +  morph_fp_sugar o Morphism.thm_morphism o Thm.transfer o Proof_Context.theory_of;
    1.17 +
    1.18  structure Data = Generic_Data
    1.19  (
    1.20    type T = fp_sugar Symtab.table;
    1.21 @@ -160,8 +164,10 @@
    1.22  
    1.23  fun fp_sugar_of ctxt =
    1.24    Symtab.lookup (Data.get (Context.Proof ctxt))
    1.25 -  #> Option.map (morph_fp_sugar
    1.26 -    (Morphism.thm_morphism (Thm.transfer (Proof_Context.theory_of ctxt))));
    1.27 +  #> Option.map (transfer_fp_sugar ctxt);
    1.28 +
    1.29 +fun fp_sugars_of ctxt =
    1.30 +  Symtab.fold (cons o transfer_fp_sugar ctxt o snd) (Data.get (Context.Proof ctxt)) [];
    1.31  
    1.32  fun co_induct_of (i :: _) = i;
    1.33  fun strong_co_induct_of [_, s] = s;