equal
deleted
inserted
replaced
1015 |
1015 |
1016 (* some peephole optimisations *) |
1016 (* some peephole optimisations *) |
1017 |
1017 |
1018 fun peephole_optimisation thy intro = |
1018 fun peephole_optimisation thy intro = |
1019 let |
1019 let |
|
1020 val ctxt = Proof_Context.init_global thy (* FIXME proper context!? *) |
1020 val process = |
1021 val process = |
1021 rewrite_rule (Predicate_Compile_Simps.get (Proof_Context.init_global thy)) |
1022 rewrite_rule ctxt (Predicate_Compile_Simps.get ctxt) |
1022 fun process_False intro_t = |
1023 fun process_False intro_t = |
1023 if member (op =) (Logic.strip_imp_prems intro_t) @{prop "False"} then NONE else SOME intro_t |
1024 if member (op =) (Logic.strip_imp_prems intro_t) @{prop "False"} then NONE else SOME intro_t |
1024 fun process_True intro_t = |
1025 fun process_True intro_t = |
1025 map_filter_premises (fn p => if p = @{prop True} then NONE else SOME p) intro_t |
1026 map_filter_premises (fn p => if p = @{prop True} then NONE else SOME p) intro_t |
1026 in |
1027 in |