unfold intermediate definitions after sealing the bnf
authortraytel
Mon Mar 10 13:23:16 2014 +0100 (2014-03-10)
changeset 560168875cdcfc85b
parent 56015 57e2cfba9c6e
child 56017 8d3df792d47e
unfold intermediate definitions after sealing the bnf
src/HOL/BNF_Comp.thy
src/HOL/Library/bnf_decl.ML
src/HOL/Tools/BNF/bnf_comp.ML
src/HOL/Tools/BNF/bnf_def.ML
src/HOL/Tools/BNF/bnf_gfp.ML
src/HOL/Tools/BNF/bnf_lfp.ML
     1.1 --- a/src/HOL/BNF_Comp.thy	Sun Mar 09 22:45:09 2014 +0100
     1.2 +++ b/src/HOL/BNF_Comp.thy	Mon Mar 10 13:23:16 2014 +0100
     1.3 @@ -147,6 +147,9 @@
     1.4  
     1.5  definition id_bnf_comp :: "'a \<Rightarrow> 'a" where "id_bnf_comp \<equiv> (\<lambda>x. x)"
     1.6  
     1.7 +lemma id_bnf_comp_apply: "id_bnf_comp x = x"
     1.8 +  unfolding id_bnf_comp_def by simp
     1.9 +
    1.10  bnf ID: 'a
    1.11    map: "id_bnf_comp :: ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b"
    1.12    sets: "\<lambda>x. {x}"
     2.1 --- a/src/HOL/Library/bnf_decl.ML	Sun Mar 09 22:45:09 2014 +0100
     2.2 +++ b/src/HOL/Library/bnf_decl.ML	Mon Mar 10 13:23:16 2014 +0100
     2.3 @@ -68,7 +68,7 @@
     2.4      val Fwits = map2 (fn witb => fn witT =>
     2.5        Const (Local_Theory.full_name lthy witb, witT)) witbs witTs;
     2.6      val (key, goals, (triv_tac_opt, wit_goalss), after_qed, lthy, _) =
     2.7 -      prepare_def Do_Inline (user_policy Note_Some) I (K I) (K I) (SOME (map TFree deads))
     2.8 +      prepare_def Do_Inline (user_policy Note_Some) false I (K I) (K I) (SOME (map TFree deads))
     2.9        user_mapb user_relb user_setbs ((((((Binding.empty, T), Fmap), Fsets), Fbd), Fwits), NONE)
    2.10        lthy;
    2.11  
     3.1 --- a/src/HOL/Tools/BNF/bnf_comp.ML	Sun Mar 09 22:45:09 2014 +0100
     3.2 +++ b/src/HOL/Tools/BNF/bnf_comp.ML	Mon Mar 10 13:23:16 2014 +0100
     3.3 @@ -338,8 +338,8 @@
     3.4          (maps wit_thms_of_bnf inners);
     3.5  
     3.6      val (bnf', lthy') =
     3.7 -      bnf_def const_policy (K Dont_Note) qualify tacs wit_tac (SOME (oDs @ flat Dss)) Binding.empty
     3.8 -        Binding.empty [] ((((((b, CCA), mapx), sets'), bd'), wits), SOME rel) lthy;
     3.9 +      bnf_def const_policy (K Dont_Note) true qualify tacs wit_tac (SOME (oDs @ flat Dss))
    3.10 +        Binding.empty Binding.empty [] ((((((b, CCA), mapx), sets'), bd'), wits), SOME rel) lthy;
    3.11  
    3.12      val phi =
    3.13        Morphism.thm_morphism "BNF" (unfold_thms lthy' [id_bnf_comp_def])
    3.14 @@ -436,8 +436,8 @@
    3.15      fun wit_tac _ = mk_simple_wit_tac (wit_thms_of_bnf bnf);
    3.16  
    3.17      val (bnf', lthy') =
    3.18 -      bnf_def Smart_Inline (K Dont_Note) qualify tacs wit_tac (SOME (killedAs @ Ds)) Binding.empty
    3.19 -        Binding.empty [] ((((((b, T), mapx), sets), bd), wits), SOME rel) lthy;
    3.20 +      bnf_def Smart_Inline (K Dont_Note) true qualify tacs wit_tac (SOME (killedAs @ Ds))
    3.21 +        Binding.empty Binding.empty [] ((((((b, T), mapx), sets), bd), wits), SOME rel) lthy;
    3.22    in
    3.23      (bnf', (add_bnf_to_unfolds bnf' unfold_set, lthy'))
    3.24    end;
    3.25 @@ -526,8 +526,8 @@
    3.26      fun wit_tac _ = mk_simple_wit_tac (wit_thms_of_bnf bnf);
    3.27  
    3.28      val (bnf', lthy') =
    3.29 -      bnf_def Smart_Inline (K Dont_Note) qualify tacs wit_tac (SOME Ds) Binding.empty Binding.empty
    3.30 -        [] ((((((b, T), mapx), sets), bd), wits), SOME rel) lthy;
    3.31 +      bnf_def Smart_Inline (K Dont_Note) true qualify tacs wit_tac (SOME Ds) Binding.empty
    3.32 +        Binding.empty [] ((((((b, T), mapx), sets), bd), wits), SOME rel) lthy;
    3.33    in
    3.34      (bnf', (add_bnf_to_unfolds bnf' unfold_set, lthy'))
    3.35    end;
    3.36 @@ -607,8 +607,8 @@
    3.37      fun wit_tac _ = mk_simple_wit_tac (wit_thms_of_bnf bnf);
    3.38  
    3.39      val (bnf', lthy') =
    3.40 -      bnf_def Smart_Inline (K Dont_Note) qualify tacs wit_tac (SOME Ds) Binding.empty Binding.empty
    3.41 -        [] ((((((b, T), mapx), sets), bd), wits), SOME rel) lthy;
    3.42 +      bnf_def Smart_Inline (K Dont_Note) true qualify tacs wit_tac (SOME Ds) Binding.empty
    3.43 +        Binding.empty [] ((((((b, T), mapx), sets), bd), wits), SOME rel) lthy;
    3.44    in
    3.45      (bnf', (add_bnf_to_unfolds bnf' unfold_set, lthy'))
    3.46    end;
    3.47 @@ -765,21 +765,6 @@
    3.48        |> mk_Frees' "f" (map2 (curry op -->) As Bs)
    3.49        ||>> mk_Frees' "R" (map2 mk_pred2T As Bs);
    3.50  
    3.51 -    val map_unfolds = map (unfold_thms lthy [id_bnf_comp_def]) (#map_unfolds unfold_set);
    3.52 -    val set_unfoldss = #set_unfoldss unfold_set;
    3.53 -    val rel_unfolds = map (unfold_thms lthy [id_bnf_comp_def]) (#rel_unfolds unfold_set);
    3.54 -
    3.55 -    val expand_maps = expand_id_bnf_comp_def o
    3.56 -      fold expand_term_const (map (single o Logic.dest_equals o Thm.prop_of) map_unfolds);
    3.57 -    val expand_sets =
    3.58 -      fold expand_term_const (map (map (Logic.dest_equals o Thm.prop_of)) set_unfoldss);
    3.59 -    val expand_rels = expand_id_bnf_comp_def o
    3.60 -      fold expand_term_const (map (single o Logic.dest_equals o Thm.prop_of) rel_unfolds);
    3.61 -    fun unfold_maps ctxt = fold (unfold_thms ctxt o single) (id_bnf_comp_def :: map_unfolds);
    3.62 -    fun unfold_sets ctxt = fold (unfold_thms ctxt) set_unfoldss;
    3.63 -    fun unfold_rels ctxt = fold (unfold_thms ctxt o single) (id_bnf_comp_def :: rel_unfolds);
    3.64 -    fun unfold_all ctxt = unfold_sets ctxt o unfold_maps ctxt o unfold_rels ctxt;
    3.65 -
    3.66      val repTA = mk_T_of_bnf Ds As bnf;
    3.67      val T_bind = qualify b;
    3.68      val TA_params = Term.add_tfreesT repTA [];
    3.69 @@ -800,12 +785,12 @@
    3.70        abs_inverse = Abs_inverse', type_definition = type_definition};
    3.71  
    3.72      val bnf_map = fold_rev Term.absfree fs' (HOLogic.mk_comp (HOLogic.mk_comp (AbsB,
    3.73 -      Term.list_comb (expand_maps (mk_map_of_bnf Ds As Bs bnf), fs)), RepA));
    3.74 -    val bnf_sets = map ((fn t => HOLogic.mk_comp (t, RepA)) o expand_maps o expand_sets)
    3.75 +      Term.list_comb (mk_map_of_bnf Ds As Bs bnf, fs)), RepA));
    3.76 +    val bnf_sets = map ((fn t => HOLogic.mk_comp (t, RepA)))
    3.77        (mk_sets_of_bnf (replicate live Ds) (replicate live As) bnf);
    3.78      val bnf_bd = mk_bd_of_bnf Ds As bnf;
    3.79      val bnf_rel = fold_rev Term.absfree Rs' (mk_vimage2p RepA RepB $
    3.80 -      (Term.list_comb (expand_rels (mk_rel_of_bnf Ds As Bs bnf), Rs)));
    3.81 +      (Term.list_comb (mk_rel_of_bnf Ds As Bs bnf, Rs)));
    3.82  
    3.83      (*bd may depend only on dead type variables*)
    3.84      val bd_repT = fst (dest_relT (fastype_of bnf_bd));
    3.85 @@ -836,24 +821,22 @@
    3.86            (bnf_bd', bd_ordIso, bd_card_order, bd_cinfinite)
    3.87          end;
    3.88  
    3.89 -    fun map_id0_tac ctxt =
    3.90 -      rtac (@{thm type_copy_map_id0} OF [type_definition, unfold_maps ctxt (map_id0_of_bnf bnf)]) 1;
    3.91 -    fun map_comp0_tac ctxt =
    3.92 -      rtac (@{thm type_copy_map_comp0} OF
    3.93 -        [type_definition, unfold_maps ctxt (map_comp0_of_bnf bnf)]) 1;
    3.94 -    fun map_cong0_tac ctxt =
    3.95 -      EVERY' (rtac @{thm type_copy_map_cong0} :: rtac (unfold_all ctxt (map_cong0_of_bnf bnf)) ::
    3.96 +    fun map_id0_tac _ =
    3.97 +      rtac (@{thm type_copy_map_id0} OF [type_definition, map_id0_of_bnf bnf]) 1;
    3.98 +    fun map_comp0_tac _ =
    3.99 +      rtac (@{thm type_copy_map_comp0} OF [type_definition, map_comp0_of_bnf bnf]) 1;
   3.100 +    fun map_cong0_tac _ =
   3.101 +      EVERY' (rtac @{thm type_copy_map_cong0} :: rtac (map_cong0_of_bnf bnf) ::
   3.102          map (fn i => EVERY' [select_prem_tac live (dtac meta_spec) i, etac meta_mp,
   3.103            etac (o_apply RS equalityD2 RS set_mp)]) (1 upto live)) 1;
   3.104 -    fun set_map0_tac thm ctxt =
   3.105 -      rtac (@{thm type_copy_set_map0} OF [type_definition, unfold_all ctxt thm]) 1;
   3.106 -    val set_bd_tacs = map (fn thm => fn ctxt => rtac (@{thm ordLeq_ordIso_trans} OF
   3.107 -        [unfold_sets ctxt thm, bd_ordIso] RS @{thm type_copy_set_bd}) 1)
   3.108 -      (set_bd_of_bnf bnf);
   3.109 -    fun le_rel_OO_tac ctxt =
   3.110 -      rtac (unfold_rels ctxt (le_rel_OO_of_bnf bnf) RS @{thm vimage2p_relcompp_mono}) 1;
   3.111 +    fun set_map0_tac thm _ =
   3.112 +      rtac (@{thm type_copy_set_map0} OF [type_definition, thm]) 1;
   3.113 +    val set_bd_tacs = map (fn thm => fn _ => rtac (@{thm ordLeq_ordIso_trans} OF
   3.114 +        [thm, bd_ordIso] RS @{thm type_copy_set_bd}) 1) (set_bd_of_bnf bnf);
   3.115 +    fun le_rel_OO_tac _ =
   3.116 +      rtac (le_rel_OO_of_bnf bnf RS @{thm vimage2p_relcompp_mono}) 1;
   3.117      fun rel_OO_Grp_tac ctxt =
   3.118 -      (rtac (unfold_all ctxt (rel_OO_Grp_of_bnf bnf) RS @{thm vimage2p_cong} RS trans) THEN'
   3.119 +      (rtac (rel_OO_Grp_of_bnf bnf RS @{thm vimage2p_cong} RS trans) THEN'
   3.120        SELECT_GOAL (unfold_thms_tac ctxt [o_apply,
   3.121          type_definition RS @{thm type_copy_vimage2p_Grp_Rep},
   3.122          type_definition RS @{thm vimage2p_relcompp_converse}]) THEN' rtac refl) 1;
   3.123 @@ -864,18 +847,40 @@
   3.124  
   3.125      val bnf_wits = map (fn (I, t) =>
   3.126          fold Term.absdummy (map (nth As) I)
   3.127 -          (AbsA $ Term.list_comb (expand_id_bnf_comp_def t, map Bound (0 upto length I - 1))))
   3.128 +          (AbsA $ Term.list_comb (t, map Bound (0 upto length I - 1))))
   3.129        (mk_wits_of_bnf (replicate nwits Ds) (replicate nwits As) bnf);
   3.130  
   3.131 -    fun wit_tac ctxt = ALLGOALS (dtac (type_definition RS @{thm type_copy_wit})) THEN
   3.132 -      mk_simple_wit_tac (map (unfold_all ctxt) (wit_thms_of_bnf bnf));
   3.133 +    fun wit_tac _ = ALLGOALS (dtac (type_definition RS @{thm type_copy_wit})) THEN
   3.134 +      mk_simple_wit_tac (wit_thms_of_bnf bnf);
   3.135  
   3.136      val (bnf', lthy') =
   3.137 -      bnf_def Hardly_Inline (user_policy Dont_Note) qualify tacs wit_tac (SOME all_deads)
   3.138 +      bnf_def Hardly_Inline (user_policy Dont_Note) true qualify tacs wit_tac (SOME all_deads)
   3.139          Binding.empty Binding.empty []
   3.140          ((((((b, TA), bnf_map), bnf_sets), bnf_bd'), bnf_wits), SOME bnf_rel) lthy;
   3.141 +
   3.142 +    val unfolds = @{thm id_bnf_comp_apply} ::
   3.143 +      (#map_unfolds unfold_set @ flat (#set_unfoldss unfold_set) @ #rel_unfolds unfold_set);
   3.144 +
   3.145 +    val bnf'' = bnf' |> morph_bnf_defs (Morphism.thm_morphism "BNF" (unfold_thms lthy' unfolds));
   3.146 +    
   3.147 +    val map_def = map_def_of_bnf bnf'';
   3.148 +    val set_defs = set_defs_of_bnf bnf'';
   3.149 +    val rel_def = map_def_of_bnf bnf'';
   3.150 +
   3.151 +    val bnf_b = qualify b;
   3.152 +    val def_qualify =
   3.153 +      Thm.def_binding o Binding.conceal o Binding.qualify false (Binding.name_of bnf_b);
   3.154 +    fun mk_prefix_binding pre = Binding.prefix_name (pre ^ "_") bnf_b;
   3.155 +    val map_b = def_qualify (mk_prefix_binding mapN);
   3.156 +    val rel_b = def_qualify (mk_prefix_binding relN);
   3.157 +    val set_bs = if live = 1 then [def_qualify (mk_prefix_binding setN)]
   3.158 +      else map (fn i => def_qualify (mk_prefix_binding (mk_setN i))) (1 upto live);
   3.159 +
   3.160 +    val notes = (map_b, map_def) :: (rel_b, rel_def) :: (set_bs ~~ set_defs)
   3.161 +      |> map (fn (b, def) => ((b, []), [([def], [])]))
   3.162 +    val lthy'' = lthy' |> Local_Theory.notes notes |> snd
   3.163    in
   3.164 -    ((bnf', (all_deads, absT_info)), lthy')
   3.165 +    ((bnf'', (all_deads, absT_info)), lthy'')
   3.166    end;
   3.167  
   3.168  exception BAD_DEAD of typ * typ;
     4.1 --- a/src/HOL/Tools/BNF/bnf_def.ML	Sun Mar 09 22:45:09 2014 +0100
     4.2 +++ b/src/HOL/Tools/BNF/bnf_def.ML	Mon Mar 10 13:23:16 2014 +0100
     4.3 @@ -12,6 +12,7 @@
     4.4    type nonemptiness_witness = {I: int list, wit: term, prop: thm list}
     4.5  
     4.6    val morph_bnf: morphism -> bnf -> bnf
     4.7 +  val morph_bnf_defs: morphism -> bnf -> bnf
     4.8    val bnf_of: Proof.context -> string -> bnf option
     4.9    val register_bnf: string -> (bnf * local_theory) -> (bnf * local_theory)
    4.10  
    4.11 @@ -100,16 +101,16 @@
    4.12      Proof.context
    4.13  
    4.14    val print_bnfs: Proof.context -> unit
    4.15 -  val prepare_def: inline_policy -> (Proof.context -> fact_policy) -> (binding -> binding) ->
    4.16 -    (Proof.context -> 'a -> typ) -> (Proof.context -> 'b -> term) -> typ list option ->
    4.17 -    binding -> binding -> binding list ->
    4.18 +  val prepare_def: inline_policy -> (Proof.context -> fact_policy) -> bool ->
    4.19 +    (binding -> binding) -> (Proof.context -> 'a -> typ) -> (Proof.context -> 'b -> term) ->
    4.20 +    typ list option -> binding -> binding -> binding list ->
    4.21      (((((binding * 'a) * 'b) * 'b list) * 'b) * 'b list) * 'b option -> Proof.context ->
    4.22      string * term list *
    4.23      ((Proof.context -> thm list -> tactic) option * term list list) *
    4.24      ((thm list -> thm list list) -> thm list list -> Proof.context -> bnf * local_theory) *
    4.25      local_theory * thm list
    4.26  
    4.27 -  val define_bnf_consts: inline_policy -> fact_policy -> typ list option ->
    4.28 +  val define_bnf_consts: inline_policy -> fact_policy -> bool -> typ list option ->
    4.29      binding -> binding -> binding list ->
    4.30      (((((binding * typ) * term) * term list) * term) * term list) * term option -> local_theory ->
    4.31        ((typ list * typ list * typ list * typ) *
    4.32 @@ -121,7 +122,7 @@
    4.33          (typ list -> typ list -> typ list -> term) *
    4.34          (typ list -> typ list -> typ list -> term))) * local_theory
    4.35  
    4.36 -  val bnf_def: inline_policy -> (Proof.context -> fact_policy) -> (binding -> binding) ->
    4.37 +  val bnf_def: inline_policy -> (Proof.context -> fact_policy) -> bool -> (binding -> binding) ->
    4.38      (Proof.context -> tactic) list ->
    4.39      (Proof.context -> tactic) -> typ list option -> binding ->
    4.40      binding -> binding list ->
    4.41 @@ -434,22 +435,27 @@
    4.42         axioms = axioms, defs = defs, facts = facts,
    4.43         nwits = length wits, wits = wits, rel = rel};
    4.44  
    4.45 -fun morph_bnf phi (BNF {name = name, T = T, live = live, lives = lives, lives' = lives',
    4.46 +fun map_bnf f1 f2 f3 f4 f5 f6 f7 f8 f9 f10 f11 f12 f13 f14 f15 f16
    4.47 +  (BNF {name = name, T = T, live = live, lives = lives, lives' = lives',
    4.48    dead = dead, deads = deads, map = map, sets = sets, bd = bd,
    4.49    axioms = axioms, defs = defs, facts = facts,
    4.50    nwits = nwits, wits = wits, rel = rel}) =
    4.51 -  BNF {name = Morphism.binding phi name, T = Morphism.typ phi T,
    4.52 -    live = live, lives = List.map (Morphism.typ phi) lives,
    4.53 -    lives' = List.map (Morphism.typ phi) lives',
    4.54 -    dead = dead, deads = List.map (Morphism.typ phi) deads,
    4.55 -    map = Morphism.term phi map, sets = List.map (Morphism.term phi) sets,
    4.56 -    bd = Morphism.term phi bd,
    4.57 -    axioms = morph_axioms phi axioms,
    4.58 -    defs = morph_defs phi defs,
    4.59 -    facts = morph_facts phi facts,
    4.60 -    nwits = nwits,
    4.61 -    wits = List.map (morph_witness phi) wits,
    4.62 -    rel = Morphism.term phi rel};
    4.63 +  BNF {name = f1 name, T = f2 T,
    4.64 +       live = f3 live, lives = f4 lives, lives' = f5 lives', dead = f6 dead, deads = f7 deads,
    4.65 +       map = f8 map, sets = f9 sets, bd = f10 bd,
    4.66 +       axioms = f11 axioms, defs = f12 defs, facts = f13 facts,
    4.67 +       nwits = f14 nwits, wits = f15 wits, rel = f16 rel};
    4.68 +
    4.69 +fun morph_bnf phi =
    4.70 +  let
    4.71 +    val Tphi = Morphism.typ phi;
    4.72 +    val tphi = Morphism.term phi;
    4.73 +  in
    4.74 +    map_bnf (Morphism.binding phi) Tphi I (map Tphi) (map Tphi) I (map Tphi) tphi (map tphi) tphi
    4.75 +      (morph_axioms phi) (morph_defs phi) (morph_facts phi) I (map (morph_witness phi)) tphi
    4.76 +  end;
    4.77 +
    4.78 +fun morph_bnf_defs phi = map_bnf I I I I I I I I I I I (morph_defs phi) I I I I;
    4.79  
    4.80  structure Data = Generic_Data
    4.81  (
    4.82 @@ -660,7 +666,7 @@
    4.83  
    4.84  (* Define new BNFs *)
    4.85  
    4.86 -fun define_bnf_consts const_policy fact_policy Ds_opt map_b rel_b set_bs
    4.87 +fun define_bnf_consts const_policy fact_policy internal Ds_opt map_b rel_b set_bs
    4.88    ((((((bnf_b, T_rhs), map_rhs), set_rhss), bd_rhs), wit_rhss), rel_rhs_opt) no_defs_lthy =
    4.89    let
    4.90      val live = length set_rhss;
    4.91 @@ -683,8 +689,9 @@
    4.92            ((rhs, Drule.reflexive_thm), lthy)
    4.93          else
    4.94            let val b = b () in
    4.95 -            apfst (apsnd snd) (Local_Theory.define ((b, NoSyn), ((Thm.def_binding b, []), rhs))
    4.96 -              lthy)
    4.97 +            apfst (apsnd snd)
    4.98 +              ((if internal then Local_Theory.define_internal else Local_Theory.define)
    4.99 +                ((b, NoSyn), ((Thm.def_binding b, []), rhs)) lthy)
   4.100            end
   4.101        end;
   4.102  
   4.103 @@ -830,8 +837,8 @@
   4.104       (mk_bnf_map, mk_bnf_t, mk_bnf_T, mk_bnf_rel, mk_OO_Grp)), lthy)
   4.105    end;
   4.106  
   4.107 -fun prepare_def const_policy mk_fact_policy qualify prep_typ prep_term Ds_opt map_b rel_b set_bs
   4.108 -  ((((((raw_bnf_b, raw_bnf_T), raw_map), raw_sets), raw_bd), raw_wits), raw_rel_opt)
   4.109 +fun prepare_def const_policy mk_fact_policy internal qualify prep_typ prep_term Ds_opt map_b rel_b
   4.110 +  set_bs ((((((raw_bnf_b, raw_bnf_T), raw_map), raw_sets), raw_bd), raw_wits), raw_rel_opt)
   4.111    no_defs_lthy =
   4.112    let
   4.113      val fact_policy = mk_fact_policy no_defs_lthy;
   4.114 @@ -861,7 +868,7 @@
   4.115       (bnf_map, bnf_sets, bnf_bd, bnf_wits, bnf_rel),
   4.116       (bnf_map_def, bnf_set_defs, bnf_bd_def, bnf_wit_defs, bnf_rel_def),
   4.117       (mk_bnf_map_Ds, mk_bnf_t_Ds, mk_bnf_T_Ds, _, mk_OO_Grp)), lthy) =
   4.118 -       define_bnf_consts const_policy fact_policy Ds_opt map_b rel_b set_bs
   4.119 +       define_bnf_consts const_policy fact_policy internal Ds_opt map_b rel_b set_bs
   4.120           ((((((bnf_b, T_rhs), map_rhs), set_rhss), bd_rhs), wit_rhss), rel_rhs_opt) no_defs_lthy;
   4.121  
   4.122      val dead = length deads;
   4.123 @@ -1304,7 +1311,7 @@
   4.124    (bnf, Local_Theory.declaration {syntax = false, pervasive = true}
   4.125      (fn phi => Data.map (Symtab.update (key, morph_bnf phi bnf))) lthy);
   4.126  
   4.127 -fun bnf_def const_policy fact_policy qualify tacs wit_tac Ds map_b rel_b set_bs =
   4.128 +fun bnf_def const_policy fact_policy internal qualify tacs wit_tac Ds map_b rel_b set_bs =
   4.129    (fn (_, goals, (triv_tac_opt, wit_goalss), after_qed, lthy, one_step_defs) =>
   4.130    let
   4.131      fun mk_wits_tac ctxt set_maps =
   4.132 @@ -1324,7 +1331,7 @@
   4.133        goals (map (fn tac => fn {context = ctxt, prems = _} =>
   4.134          unfold_thms_tac ctxt one_step_defs THEN tac ctxt) tacs)
   4.135      |> (fn thms => after_qed mk_wit_thms (map single thms) lthy)
   4.136 -  end) oo prepare_def const_policy fact_policy qualify (K I) (K I) Ds map_b rel_b set_bs;
   4.137 +  end) oo prepare_def const_policy fact_policy internal qualify (K I) (K I) Ds map_b rel_b set_bs;
   4.138  
   4.139  val bnf_cmd = (fn (key, goals, (triv_tac_opt, wit_goalss), after_qed, lthy, defs) =>
   4.140    let
   4.141 @@ -1343,8 +1350,8 @@
   4.142      Proof.unfolding ([[(defs, [])]])
   4.143        (Proof.theorem NONE (snd o register_bnf key oo after_qed mk_wit_thms)
   4.144          (map (single o rpair []) goals @ nontriv_wit_goals) lthy)
   4.145 -  end) oo prepare_def Do_Inline (user_policy Note_Some) I Syntax.read_typ Syntax.read_term NONE
   4.146 -    Binding.empty Binding.empty [];
   4.147 +  end) oo prepare_def Do_Inline (user_policy Note_Some) false I Syntax.read_typ Syntax.read_term
   4.148 +    NONE Binding.empty Binding.empty [];
   4.149  
   4.150  fun print_bnfs ctxt =
   4.151    let
     5.1 --- a/src/HOL/Tools/BNF/bnf_gfp.ML	Sun Mar 09 22:45:09 2014 +0100
     5.2 +++ b/src/HOL/Tools/BNF/bnf_gfp.ML	Mon Mar 10 13:23:16 2014 +0100
     5.3 @@ -2088,7 +2088,7 @@
     5.4          val (Jbnf_consts, lthy) =
     5.5            fold_map8 (fn b => fn map_b => fn rel_b => fn set_bs => fn mapx => fn sets => fn wits =>
     5.6                fn T => fn lthy =>
     5.7 -            define_bnf_consts Dont_Inline (user_policy Note_Some lthy) (SOME deads)
     5.8 +            define_bnf_consts Dont_Inline (user_policy Note_Some lthy) false (SOME deads)
     5.9                map_b rel_b set_bs
    5.10                ((((((b, T), fold_rev Term.absfree fs' mapx), sets), sbd), wits), NONE) lthy)
    5.11            bs map_bs rel_bs set_bss fs_maps setss_by_bnf all_witss Ts lthy;
    5.12 @@ -2516,7 +2516,7 @@
    5.13          val (Jbnfs, lthy) =
    5.14            fold_map7 (fn b => fn tacs => fn map_b => fn rel_b => fn set_bs => fn Jwit_thms =>
    5.15                fn consts => fn lthy =>
    5.16 -            bnf_def Do_Inline (user_policy Note_Some) I tacs (wit_tac Jwit_thms) (SOME deads)
    5.17 +            bnf_def Do_Inline (user_policy Note_Some) false I tacs (wit_tac Jwit_thms) (SOME deads)
    5.18                map_b rel_b set_bs consts lthy
    5.19              |> register_bnf (Local_Theory.full_name lthy b))
    5.20            bs tacss map_bs rel_bs set_bss Jwit_thmss
     6.1 --- a/src/HOL/Tools/BNF/bnf_lfp.ML	Sun Mar 09 22:45:09 2014 +0100
     6.2 +++ b/src/HOL/Tools/BNF/bnf_lfp.ML	Mon Mar 10 13:23:16 2014 +0100
     6.3 @@ -1483,7 +1483,7 @@
     6.4          val (Ibnf_consts, lthy) =
     6.5            fold_map8 (fn b => fn map_b => fn rel_b => fn set_bs => fn mapx => fn sets => fn wits =>
     6.6                fn T => fn lthy =>
     6.7 -            define_bnf_consts Dont_Inline (user_policy Note_Some lthy) (SOME deads)
     6.8 +            define_bnf_consts Dont_Inline (user_policy Note_Some lthy) false (SOME deads)
     6.9                map_b rel_b set_bs
    6.10                ((((((b, T), fold_rev Term.absfree fs' mapx), sets), sbd), wits), NONE) lthy)
    6.11            bs map_bs rel_bs set_bss fs_maps setss_by_bnf ctor_witss Ts lthy;
    6.12 @@ -1769,7 +1769,7 @@
    6.13  
    6.14          val (Ibnfs, lthy) =
    6.15            fold_map6 (fn b => fn tacs => fn map_b => fn rel_b => fn set_bs => fn consts => fn lthy =>
    6.16 -            bnf_def Do_Inline (user_policy Note_Some) I tacs wit_tac (SOME deads)
    6.17 +            bnf_def Do_Inline (user_policy Note_Some) false I tacs wit_tac (SOME deads)
    6.18                map_b rel_b set_bs consts lthy
    6.19              |> register_bnf (Local_Theory.full_name lthy b))
    6.20            bs tacss map_bs rel_bs set_bss