src/HOL/BNF/Tools/bnf_comp.ML
changeset 51758 55963309557b
parent 51757 7babcb61aa5c
child 51761 4c9f08836d87
     1.1 --- a/src/HOL/BNF/Tools/bnf_comp.ML	Wed Apr 24 13:16:20 2013 +0200
     1.2 +++ b/src/HOL/BNF/Tools/bnf_comp.ML	Wed Apr 24 13:16:21 2013 +0200
     1.3 @@ -261,8 +261,8 @@
     1.4          (maps wit_thms_of_bnf inners);
     1.5  
     1.6      val (bnf', lthy') =
     1.7 -      bnf_def const_policy (K Dont_Note) qualify tacs wit_tac (SOME (oDs @ flat Dss)) []
     1.8 -        (((((b, mapx), sets), bd), wits), SOME rel) lthy;
     1.9 +      bnf_def const_policy (K Dont_Note) qualify tacs wit_tac (SOME (oDs @ flat Dss)) Binding.empty
    1.10 +        [] (((((b, mapx), sets), bd), wits), SOME rel) lthy;
    1.11    in
    1.12      (bnf', (add_bnf_to_unfolds bnf' unfold_set, lthy'))
    1.13    end;
    1.14 @@ -359,8 +359,8 @@
    1.15      fun wit_tac _ = mk_simple_wit_tac (wit_thms_of_bnf bnf);
    1.16  
    1.17      val (bnf', lthy') =
    1.18 -      bnf_def Smart_Inline (K Dont_Note) qualify tacs wit_tac (SOME (killedAs @ Ds)) []
    1.19 -        (((((b, mapx), sets), Term.absdummy T bd), wits), SOME rel) lthy;
    1.20 +      bnf_def Smart_Inline (K Dont_Note) qualify tacs wit_tac (SOME (killedAs @ Ds)) Binding.empty
    1.21 +        [] (((((b, mapx), sets), Term.absdummy T bd), wits), SOME rel) lthy;
    1.22    in
    1.23      (bnf', (add_bnf_to_unfolds bnf' unfold_set, lthy'))
    1.24    end;
    1.25 @@ -443,7 +443,7 @@
    1.26      fun wit_tac _ = mk_simple_wit_tac (wit_thms_of_bnf bnf);
    1.27  
    1.28      val (bnf', lthy') =
    1.29 -      bnf_def Smart_Inline (K Dont_Note) qualify tacs wit_tac (SOME Ds) []
    1.30 +      bnf_def Smart_Inline (K Dont_Note) qualify tacs wit_tac (SOME Ds) Binding.empty []
    1.31          (((((b, mapx), sets), Term.absdummy T bd), wits), SOME rel) lthy;
    1.32  
    1.33    in
    1.34 @@ -520,7 +520,7 @@
    1.35      fun wit_tac _ = mk_simple_wit_tac (wit_thms_of_bnf bnf);
    1.36  
    1.37      val (bnf', lthy') =
    1.38 -      bnf_def Smart_Inline (K Dont_Note) qualify tacs wit_tac (SOME Ds) []
    1.39 +      bnf_def Smart_Inline (K Dont_Note) qualify tacs wit_tac (SOME Ds) Binding.empty []
    1.40          (((((b, mapx), sets), Term.absdummy T bd), wits), SOME rel) lthy;
    1.41    in
    1.42      (bnf', (add_bnf_to_unfolds bnf' unfold_set, lthy'))
    1.43 @@ -662,7 +662,8 @@
    1.44  
    1.45      fun wit_tac _ = mk_simple_wit_tac (map unfold_all (wit_thms_of_bnf bnf));
    1.46  
    1.47 -    val (bnf', lthy') = bnf_def Hardly_Inline (user_policy Dont_Note) I tacs wit_tac (SOME deads) []
    1.48 +    val (bnf', lthy') = bnf_def Hardly_Inline (user_policy Dont_Note) I tacs wit_tac (SOME deads)
    1.49 +      Binding.empty []
    1.50        (((((b, bnf_map), bnf_sets), Term.absdummy T bnf_bd'), bnf_wits), SOME bnf_rel) lthy;
    1.51    in
    1.52      ((bnf', deads), lthy')