src/HOL/BNF/Tools/bnf_fp_def_sugar.ML
changeset 51745 a06a3c777add
parent 51551 88d1d19fb74f
child 51746 5af40820948b
     1.1 --- a/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Tue Apr 23 17:13:14 2013 +0200
     1.2 +++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Tue Apr 23 17:15:44 2013 +0200
     1.3 @@ -550,8 +550,8 @@
     1.4  
     1.5              fun mk_rel_thm postproc ctr_defs' cxIn cyIn =
     1.6                fold_thms lthy ctr_defs'
     1.7 -                 (unfold_thms lthy (pre_rel_def :: (if lfp then [] else [dtor_ctor]) @
     1.8 -                      sum_prod_thms_rel)
     1.9 +                 (unfold_thms lthy (@{thm Inl_Inr_False} :: pre_rel_def ::
    1.10 +                      (if lfp then [] else [dtor_ctor]) @ sum_prod_thms_rel)
    1.11                      (cterm_instantiate_pos (nones @ [SOME cxIn, SOME cyIn]) fp_rel_thm))
    1.12                |> postproc
    1.13                |> singleton (Proof_Context.export names_lthy no_defs_lthy);