src/HOL/BNF/Tools/bnf_fp_def_sugar.ML
changeset 53126 f4d2c64c7aa8
parent 53106 d81211f61a1b
child 53143 ba80154a1118
     1.1 --- a/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Wed Aug 21 12:28:34 2013 +0200
     1.2 +++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Wed Aug 21 13:48:25 2013 +0200
     1.3 @@ -140,7 +140,10 @@
     1.4    val merge = Symtab.merge eq_fp_sugar;
     1.5  );
     1.6  
     1.7 -val fp_sugar_of = Symtab.lookup o Data.get o Context.Proof;
     1.8 +fun fp_sugar_of ctxt =
     1.9 +  Symtab.lookup (Data.get (Context.Proof ctxt))
    1.10 +  #> Option.map (morph_fp_sugar
    1.11 +    (Morphism.thm_morphism (Thm.transfer (Proof_Context.theory_of ctxt))));
    1.12  
    1.13  fun co_induct_of (i :: _) = i;
    1.14  fun strong_co_induct_of [_, s] = s;