--- a/src/HOL/BNF/Tools/bnf_comp.ML Wed Apr 24 17:47:22 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_comp.ML Wed Apr 24 18:49:52 2013 +0200
@@ -262,7 +262,7 @@
val (bnf', lthy') =
bnf_def const_policy (K Dont_Note) qualify tacs wit_tac (SOME (oDs @ flat Dss)) Binding.empty
- [] (((((b, mapx), sets), bd), wits), SOME rel) lthy;
+ Binding.empty [] (((((b, mapx), sets), bd), wits), SOME rel) lthy;
in
(bnf', (add_bnf_to_unfolds bnf' unfold_set, lthy'))
end;
@@ -360,7 +360,7 @@
val (bnf', lthy') =
bnf_def Smart_Inline (K Dont_Note) qualify tacs wit_tac (SOME (killedAs @ Ds)) Binding.empty
- [] (((((b, mapx), sets), Term.absdummy T bd), wits), SOME rel) lthy;
+ Binding.empty [] (((((b, mapx), sets), Term.absdummy T bd), wits), SOME rel) lthy;
in
(bnf', (add_bnf_to_unfolds bnf' unfold_set, lthy'))
end;
@@ -443,8 +443,8 @@
fun wit_tac _ = mk_simple_wit_tac (wit_thms_of_bnf bnf);
val (bnf', lthy') =
- bnf_def Smart_Inline (K Dont_Note) qualify tacs wit_tac (SOME Ds) Binding.empty []
- (((((b, mapx), sets), Term.absdummy T bd), wits), SOME rel) lthy;
+ bnf_def Smart_Inline (K Dont_Note) qualify tacs wit_tac (SOME Ds) Binding.empty Binding.empty
+ [] (((((b, mapx), sets), Term.absdummy T bd), wits), SOME rel) lthy;
in
(bnf', (add_bnf_to_unfolds bnf' unfold_set, lthy'))
@@ -520,8 +520,8 @@
fun wit_tac _ = mk_simple_wit_tac (wit_thms_of_bnf bnf);
val (bnf', lthy') =
- bnf_def Smart_Inline (K Dont_Note) qualify tacs wit_tac (SOME Ds) Binding.empty []
- (((((b, mapx), sets), Term.absdummy T bd), wits), SOME rel) lthy;
+ bnf_def Smart_Inline (K Dont_Note) qualify tacs wit_tac (SOME Ds) Binding.empty Binding.empty
+ [] (((((b, mapx), sets), Term.absdummy T bd), wits), SOME rel) lthy;
in
(bnf', (add_bnf_to_unfolds bnf' unfold_set, lthy'))
end;
@@ -663,7 +663,7 @@
fun wit_tac _ = mk_simple_wit_tac (map unfold_all (wit_thms_of_bnf bnf));
val (bnf', lthy') = bnf_def Hardly_Inline (user_policy Dont_Note) I tacs wit_tac (SOME deads)
- Binding.empty []
+ Binding.empty Binding.empty []
(((((b, bnf_map), bnf_sets), Term.absdummy T bnf_bd'), bnf_wits), SOME bnf_rel) lthy;
in
((bnf', deads), lthy')