src/Provers/typedsimp.ML
changeset 15570 8d8c70b41bab
parent 0 a5a9c433f639
child 15574 b1d1b5bfc464
equal deleted inserted replaced
15569:1b3115d1a8df 15570:8d8c70b41bab
    68 fun add_rule (rl, (simp_rls, other_rls)) =
    68 fun add_rule (rl, (simp_rls, other_rls)) =
    69     (simp_rule rl :: resimp_rule rl :: simp_rls, other_rls)
    69     (simp_rule rl :: resimp_rule rl :: simp_rls, other_rls)
    70     handle THM _ => (simp_rls, rl :: other_rls);
    70     handle THM _ => (simp_rls, rl :: other_rls);
    71 
    71 
    72 (*Given the list rls, return the pair (simp_rls, other_rls).*)
    72 (*Given the list rls, return the pair (simp_rls, other_rls).*)
    73 fun process_rules rls = foldr add_rule (rls, ([],[]));
    73 fun process_rules rls = Library.foldr add_rule (rls, ([],[]));
    74 
    74 
    75 (*Given list of rewrite rules, return list of both forms, reject others*)
    75 (*Given list of rewrite rules, return list of both forms, reject others*)
    76 fun process_rewrites rls = 
    76 fun process_rewrites rls = 
    77   case process_rules rls of
    77   case process_rules rls of
    78       (simp_rls,[])  =>  simp_rls
    78       (simp_rls,[])  =>  simp_rls