src/Pure/raw_simplifier.ML
changeset 54982 b327bf0dabfb
parent 54895 515630483010
child 54984 da70ab8531f4
     1.1 --- a/src/Pure/raw_simplifier.ML	Fri Jan 10 16:20:06 2014 +0100
     1.2 +++ b/src/Pure/raw_simplifier.ML	Fri Jan 10 16:55:37 2014 +0100
     1.3 @@ -604,26 +604,26 @@
     1.4      else rrule_eq_True ctxt thm name lhs elhs rhs thm
     1.5    end;
     1.6  
     1.7 -fun extract_rews (ctxt, thms) =
     1.8 +fun extract_rews ctxt thms =
     1.9    let val Simpset (_, {mk_rews = {mk, ...}, ...}) = simpset_of ctxt
    1.10    in maps (fn thm => map (rpair (Thm.get_name_hint thm)) (mk ctxt thm)) thms end;
    1.11  
    1.12 -fun extract_safe_rrules (ctxt, thm) =
    1.13 -  maps (orient_rrule ctxt) (extract_rews (ctxt, [thm]));
    1.14 +fun extract_safe_rrules ctxt thm =
    1.15 +  maps (orient_rrule ctxt) (extract_rews ctxt [thm]);
    1.16  
    1.17  
    1.18  (* add/del rules explicitly *)
    1.19  
    1.20 -fun comb_simps comb mk_rrule (ctxt, thms) =
    1.21 +fun comb_simps ctxt comb mk_rrule thms =
    1.22    let
    1.23 -    val rews = extract_rews (ctxt, thms);
    1.24 +    val rews = extract_rews ctxt thms;
    1.25    in fold (fold comb o mk_rrule) rews ctxt end;
    1.26  
    1.27  fun ctxt addsimps thms =
    1.28 -  comb_simps insert_rrule (mk_rrule ctxt) (ctxt, thms);
    1.29 +  comb_simps ctxt insert_rrule (mk_rrule ctxt) thms;
    1.30  
    1.31  fun ctxt delsimps thms =
    1.32 -  comb_simps del_rrule (map mk_rrule2 o mk_rrule ctxt) (ctxt, thms);
    1.33 +  comb_simps ctxt del_rrule (map mk_rrule2 o mk_rrule ctxt) thms;
    1.34  
    1.35  fun add_simp thm ctxt = ctxt addsimps [thm];
    1.36  fun del_simp thm ctxt = ctxt delsimps [thm];
    1.37 @@ -1197,7 +1197,7 @@
    1.38          prem; ([], NONE))
    1.39        else
    1.40          let val asm = Thm.assume prem
    1.41 -        in (extract_safe_rrules (ctxt, asm), SOME asm) end
    1.42 +        in (extract_safe_rrules ctxt asm, SOME asm) end
    1.43  
    1.44      and add_rrules (rrss, asms) ctxt =
    1.45        (fold o fold) insert_rrule rrss ctxt |> add_prems (map_filter I asms)