src/HOL/BNF/Tools/bnf_fp_def_sugar.ML
changeset 51766 f19a4d0ab1bf
parent 51758 55963309557b
child 51767 bbcdd8519253
     1.1 --- a/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Wed Apr 24 17:03:43 2013 +0200
     1.2 +++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Wed Apr 24 17:47:22 2013 +0200
     1.3 @@ -287,8 +287,8 @@
     1.4      val nested_map_comp's = map map_comp'_of_bnf nested_bnfs;
     1.5      val nested_map_ids'' = map (unfold_thms lthy @{thms id_def} o map_id_of_bnf) nested_bnfs;
     1.6      val nesting_map_ids'' = map (unfold_thms lthy @{thms id_def} o map_id_of_bnf) nesting_bnfs;
     1.7 -    val nested_set_natural's = maps set_natural'_of_bnf nested_bnfs;
     1.8 -    val nesting_set_natural's = maps set_natural'_of_bnf nesting_bnfs;
     1.9 +    val nested_set_map's = maps set_map'_of_bnf nested_bnfs;
    1.10 +    val nesting_set_map's = maps set_map'_of_bnf nesting_bnfs;
    1.11  
    1.12      val live = live_of_bnf any_fp_bnf;
    1.13  
    1.14 @@ -548,7 +548,7 @@
    1.15  
    1.16              fun mk_set_thm fp_set_thm ctr_def' cxIn =
    1.17                fold_thms lthy [ctr_def']
    1.18 -                (unfold_thms lthy (pre_set_defs @ nested_set_natural's @ nesting_set_natural's @
    1.19 +                (unfold_thms lthy (pre_set_defs @ nested_set_map's @ nesting_set_map's @
    1.20                       (if lfp then [] else [dtor_ctor]) @ sum_prod_thms_set)
    1.21                     (cterm_instantiate_pos [SOME cxIn] fp_set_thm))
    1.22                |> singleton (Proof_Context.export names_lthy no_defs_lthy);
    1.23 @@ -814,8 +814,8 @@
    1.24  
    1.25              val thm =
    1.26                Goal.prove_sorry lthy [] [] goal (fn {context = ctxt, ...} =>
    1.27 -                mk_induct_tac ctxt nn ns mss kksss (flat ctr_defss) ctor_induct'
    1.28 -                  nested_set_natural's pre_set_defss)
    1.29 +                mk_induct_tac ctxt nn ns mss kksss (flat ctr_defss) ctor_induct' nested_set_map's
    1.30 +                  pre_set_defss)
    1.31                |> singleton (Proof_Context.export names_lthy lthy)
    1.32                |> Thm.close_derivation;
    1.33            in