made SML/NJ happier
authortraytel
Thu Oct 04 17:26:04 2012 +0200 (2012-10-04)
changeset 497142c7c32f34220
parent 49713 3d07ddf70f8b
child 49715 16d8c6d288bc
made SML/NJ happier
src/HOL/BNF/Tools/bnf_comp.ML
     1.1 --- a/src/HOL/BNF/Tools/bnf_comp.ML	Thu Oct 04 17:16:55 2012 +0200
     1.2 +++ b/src/HOL/BNF/Tools/bnf_comp.ML	Thu Oct 04 17:26:04 2012 +0200
     1.3 @@ -176,7 +176,8 @@
     1.4        else
     1.5          map (fn goal =>
     1.6            Skip_Proof.prove lthy [] [] goal
     1.7 -            (fn {context, ...} => (mk_comp_set_alt_tac context (collect_set_natural_of_bnf outer)))
     1.8 +            (fn {context = ctxt, prems = _} =>
     1.9 +              mk_comp_set_alt_tac ctxt (collect_set_natural_of_bnf outer))
    1.10            |> Thm.close_derivation)
    1.11          (map2 (curry (HOLogic.mk_Trueprop o HOLogic.mk_eq)) sets sets_alt);
    1.12  
    1.13 @@ -197,8 +198,8 @@
    1.14            val single_set_bd_thmss =
    1.15              map ((fn f => map f (0 upto olive - 1)) o single_set_bd_thm) (0 upto ilive - 1);
    1.16          in
    1.17 -          map2 (fn set_alt => fn single_set_bds => fn {context, ...} =>
    1.18 -            mk_comp_set_bd_tac context set_alt single_set_bds)
    1.19 +          map2 (fn set_alt => fn single_set_bds => fn {context = ctxt, prems = _} =>
    1.20 +            mk_comp_set_bd_tac ctxt set_alt single_set_bds)
    1.21            set_alt_thms single_set_bd_thmss
    1.22          end;
    1.23  
    1.24 @@ -209,7 +210,7 @@
    1.25          val goal = fold_rev Logic.all Asets (mk_Trueprop_eq (inx, in_alt));
    1.26        in
    1.27          Skip_Proof.prove lthy [] [] goal
    1.28 -          (fn {context, ...} => mk_comp_in_alt_tac context set_alt_thms)
    1.29 +          (fn {context = ctxt, prems = _} => mk_comp_in_alt_tac ctxt set_alt_thms)
    1.30          |> Thm.close_derivation
    1.31        end;
    1.32  
    1.33 @@ -255,7 +256,7 @@
    1.34        |> minimize_wits
    1.35        |> map (fn (frees, t) => fold absfree frees t);
    1.36  
    1.37 -    fun wit_tac {context = ctxt, ...} =
    1.38 +    fun wit_tac {context = ctxt, prems = _} =
    1.39        mk_comp_wit_tac ctxt (wit_thms_of_bnf outer) (collect_set_natural_of_bnf outer)
    1.40          (maps wit_thms_of_bnf inners);
    1.41  
    1.42 @@ -305,11 +306,11 @@
    1.43        (Library.foldr1 (uncurry mk_csum) (map (mk_card_of o HOLogic.mk_UNIV) killedAs)) bnf_bd;
    1.44  
    1.45      fun map_id_tac _ = rtac (map_id_of_bnf bnf) 1;
    1.46 -    fun map_comp_tac {context, ...} =
    1.47 -      unfold_thms_tac context ((map_comp_of_bnf bnf RS sym) :: @{thms o_assoc id_o o_id}) THEN
    1.48 +    fun map_comp_tac {context = ctxt, prems = _} =
    1.49 +      unfold_thms_tac ctxt ((map_comp_of_bnf bnf RS sym) :: @{thms o_assoc id_o o_id}) THEN
    1.50        rtac refl 1;
    1.51 -    fun map_cong_tac {context, ...} =
    1.52 -      mk_kill_map_cong_tac context n (live - n) (map_cong_of_bnf bnf);
    1.53 +    fun map_cong_tac {context = ctxt, prems = _} =
    1.54 +      mk_kill_map_cong_tac ctxt n (live - n) (map_cong_of_bnf bnf);
    1.55      val set_natural_tacs = map (fn thm => fn _ => rtac thm 1) (drop n (set_natural_of_bnf bnf));
    1.56      fun bd_card_order_tac _ = mk_kill_bd_card_order_tac n (bd_card_order_of_bnf bnf);
    1.57      fun bd_cinfinite_tac _ = mk_kill_bd_cinfinite_tac (bd_Cinfinite_of_bnf bnf);
    1.58 @@ -399,11 +400,11 @@
    1.59      val bd = mk_bd_of_bnf Ds As bnf;
    1.60  
    1.61      fun map_id_tac _ = rtac (map_id_of_bnf bnf) 1;
    1.62 -    fun map_comp_tac {context, ...} =
    1.63 -      unfold_thms_tac context ((map_comp_of_bnf bnf RS sym) :: @{thms o_assoc id_o o_id}) THEN
    1.64 +    fun map_comp_tac {context = ctxt, prems = _} =
    1.65 +      unfold_thms_tac ctxt ((map_comp_of_bnf bnf RS sym) :: @{thms o_assoc id_o o_id}) THEN
    1.66        rtac refl 1;
    1.67 -    fun map_cong_tac {context, ...} =
    1.68 -      rtac (map_cong_of_bnf bnf) 1 THEN REPEAT_DETERM_N live (Goal.assume_rule_tac context 1);
    1.69 +    fun map_cong_tac {context = ctxt, prems = _} =
    1.70 +      rtac (map_cong_of_bnf bnf) 1 THEN REPEAT_DETERM_N live (Goal.assume_rule_tac ctxt 1);
    1.71      val set_natural_tacs =
    1.72        if ! quick_and_dirty then
    1.73          replicate (n + live) (K all_tac)
    1.74 @@ -487,8 +488,8 @@
    1.75  
    1.76      fun map_id_tac _ = rtac (map_id_of_bnf bnf) 1;
    1.77      fun map_comp_tac _ = rtac (map_comp_of_bnf bnf) 1;
    1.78 -    fun map_cong_tac {context, ...} =
    1.79 -      rtac (map_cong_of_bnf bnf) 1 THEN REPEAT_DETERM_N live (Goal.assume_rule_tac context 1);
    1.80 +    fun map_cong_tac {context = ctxt, prems = _} =
    1.81 +      rtac (map_cong_of_bnf bnf) 1 THEN REPEAT_DETERM_N live (Goal.assume_rule_tac ctxt 1);
    1.82      val set_natural_tacs = permute (map (fn thm => fn _ => rtac thm 1) (set_natural_of_bnf bnf));
    1.83      fun bd_card_order_tac _ = rtac (bd_card_order_of_bnf bnf) 1;
    1.84      fun bd_cinfinite_tac _ = rtac (bd_cinfinite_of_bnf bnf) 1;