src/HOL/BNF/Tools/bnf_comp.ML
changeset 51767 bbcdd8519253
parent 51766 f19a4d0ab1bf
child 51782 84e7225f5ab6
     1.1 --- a/src/HOL/BNF/Tools/bnf_comp.ML	Wed Apr 24 17:47:22 2013 +0200
     1.2 +++ b/src/HOL/BNF/Tools/bnf_comp.ML	Wed Apr 24 18:49:52 2013 +0200
     1.3 @@ -262,7 +262,7 @@
     1.4  
     1.5      val (bnf', lthy') =
     1.6        bnf_def const_policy (K Dont_Note) qualify tacs wit_tac (SOME (oDs @ flat Dss)) Binding.empty
     1.7 -        [] (((((b, mapx), sets), bd), wits), SOME rel) lthy;
     1.8 +        Binding.empty [] (((((b, mapx), sets), bd), wits), SOME rel) lthy;
     1.9    in
    1.10      (bnf', (add_bnf_to_unfolds bnf' unfold_set, lthy'))
    1.11    end;
    1.12 @@ -360,7 +360,7 @@
    1.13  
    1.14      val (bnf', lthy') =
    1.15        bnf_def Smart_Inline (K Dont_Note) qualify tacs wit_tac (SOME (killedAs @ Ds)) Binding.empty
    1.16 -        [] (((((b, mapx), sets), Term.absdummy T bd), wits), SOME rel) lthy;
    1.17 +        Binding.empty [] (((((b, mapx), sets), Term.absdummy T bd), wits), SOME rel) lthy;
    1.18    in
    1.19      (bnf', (add_bnf_to_unfolds bnf' unfold_set, lthy'))
    1.20    end;
    1.21 @@ -443,8 +443,8 @@
    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 Dont_Note) qualify tacs wit_tac (SOME Ds) Binding.empty []
    1.26 -        (((((b, mapx), sets), Term.absdummy T bd), wits), SOME rel) lthy;
    1.27 +      bnf_def Smart_Inline (K Dont_Note) qualify tacs wit_tac (SOME Ds) Binding.empty Binding.empty
    1.28 +        [] (((((b, mapx), sets), Term.absdummy T bd), wits), SOME rel) lthy;
    1.29  
    1.30    in
    1.31      (bnf', (add_bnf_to_unfolds bnf' unfold_set, lthy'))
    1.32 @@ -520,8 +520,8 @@
    1.33      fun wit_tac _ = mk_simple_wit_tac (wit_thms_of_bnf bnf);
    1.34  
    1.35      val (bnf', lthy') =
    1.36 -      bnf_def Smart_Inline (K Dont_Note) qualify tacs wit_tac (SOME Ds) Binding.empty []
    1.37 -        (((((b, mapx), sets), Term.absdummy T bd), wits), SOME rel) lthy;
    1.38 +      bnf_def Smart_Inline (K Dont_Note) qualify tacs wit_tac (SOME Ds) Binding.empty Binding.empty
    1.39 +        [] (((((b, mapx), sets), Term.absdummy T bd), wits), SOME rel) lthy;
    1.40    in
    1.41      (bnf', (add_bnf_to_unfolds bnf' unfold_set, lthy'))
    1.42    end;
    1.43 @@ -663,7 +663,7 @@
    1.44      fun wit_tac _ = mk_simple_wit_tac (map unfold_all (wit_thms_of_bnf bnf));
    1.45  
    1.46      val (bnf', lthy') = bnf_def Hardly_Inline (user_policy Dont_Note) I tacs wit_tac (SOME deads)
    1.47 -      Binding.empty []
    1.48 +      Binding.empty Binding.empty []
    1.49        (((((b, bnf_map), bnf_sets), Term.absdummy T bnf_bd'), bnf_wits), SOME bnf_rel) lthy;
    1.50    in
    1.51      ((bnf', deads), lthy')