File ‹More_Simplifier.ML›
structure More_Simplifier =
struct
fun asm_full_var_simplify ctxt thm =
let
val ((_, [thm']), ctxt') = Variable.import false [thm] ctxt
in
Simplifier.full_simplify ctxt' thm'
|> singleton (Variable.export ctxt' ctxt)
|> Drule.zero_var_indexes
end;
fun var_simplify_only ctxt ths thm =
asm_full_var_simplify (Raw_Simplifier.clear_simpset ctxt addsimps ths) thm;
val var_simplified = Attrib.thms >>
(fn ths => Thm.rule_attribute ths
(fn context => var_simplify_only (Context.proof_of context) ths));
fun rewrite_simp_opt ctxt simp_spec_opt = case simp_spec_opt of
SOME simp_spec => var_simplify_only ctxt simp_spec
| NONE => Simplifier.full_simplify ctxt;
end;