src/HOL/BNF/Tools/bnf_comp.ML
changeset 49538 c90818b63599
parent 49512 82d99fe04018
child 49585 5c4a12550491
     1.1 --- a/src/HOL/BNF/Tools/bnf_comp.ML	Sun Sep 23 14:52:53 2012 +0200
     1.2 +++ b/src/HOL/BNF/Tools/bnf_comp.ML	Sun Sep 23 14:52:53 2012 +0200
     1.3 @@ -270,7 +270,7 @@
     1.4          (maps wit_thms_of_bnf inners);
     1.5  
     1.6      val (bnf', lthy') =
     1.7 -      bnf_def const_policy (K Derive_Few_Facts) qualify tacs wit_tac (SOME (oDs @ flat Dss))
     1.8 +      bnf_def const_policy (K Dont_Note) qualify tacs wit_tac (SOME (oDs @ flat Dss))
     1.9          (((((b, mapx), sets), bd), wits), SOME rel) lthy;
    1.10    in
    1.11      (bnf', (add_bnf_to_unfolds bnf' unfold_set, lthy'))
    1.12 @@ -368,7 +368,7 @@
    1.13      fun wit_tac _ = mk_simple_wit_tac (wit_thms_of_bnf bnf);
    1.14  
    1.15      val (bnf', lthy') =
    1.16 -      bnf_def Smart_Inline (K Derive_Few_Facts) qualify tacs wit_tac (SOME (killedAs @ Ds))
    1.17 +      bnf_def Smart_Inline (K Dont_Note) qualify tacs wit_tac (SOME (killedAs @ Ds))
    1.18          (((((b, mapx), sets), Term.absdummy T bd), wits), SOME rel) lthy;
    1.19    in
    1.20      (bnf', (add_bnf_to_unfolds bnf' unfold_set, lthy'))
    1.21 @@ -452,7 +452,7 @@
    1.22      fun wit_tac _ = mk_simple_wit_tac (wit_thms_of_bnf bnf);
    1.23  
    1.24      val (bnf', lthy') =
    1.25 -      bnf_def Smart_Inline (K Derive_Few_Facts) qualify tacs wit_tac (SOME Ds)
    1.26 +      bnf_def Smart_Inline (K Dont_Note) qualify tacs wit_tac (SOME Ds)
    1.27          (((((b, mapx), sets), Term.absdummy T bd), wits), SOME rel) lthy;
    1.28  
    1.29    in
    1.30 @@ -529,7 +529,7 @@
    1.31      fun wit_tac _ = mk_simple_wit_tac (wit_thms_of_bnf bnf);
    1.32  
    1.33      val (bnf', lthy') =
    1.34 -      bnf_def Smart_Inline (K Derive_Few_Facts) qualify tacs wit_tac (SOME Ds)
    1.35 +      bnf_def Smart_Inline (K Dont_Note) qualify tacs wit_tac (SOME Ds)
    1.36          (((((b, mapx), sets), Term.absdummy T bd), wits), SOME rel) lthy;
    1.37    in
    1.38      (bnf', (add_bnf_to_unfolds bnf' unfold_set, lthy'))
    1.39 @@ -671,9 +671,7 @@
    1.40  
    1.41      fun wit_tac _ = mk_simple_wit_tac (map unfold_all (wit_thms_of_bnf bnf));
    1.42  
    1.43 -    val policy = user_policy Derive_All_Facts;
    1.44 -
    1.45 -    val (bnf', lthy') = bnf_def Hardly_Inline policy I tacs wit_tac (SOME deads)
    1.46 +    val (bnf', lthy') = bnf_def Hardly_Inline (user_policy Dont_Note) I tacs wit_tac (SOME deads)
    1.47        (((((b, bnf_map), bnf_sets), Term.absdummy T bnf_bd'), bnf_wits), SOME bnf_rel) lthy;
    1.48    in
    1.49      ((bnf', deads), lthy')