equal
deleted
inserted
replaced
428 |
428 |
429 fun eq_morphism _ [] = NONE |
429 fun eq_morphism _ [] = NONE |
430 | eq_morphism ctxt0 thms = |
430 | eq_morphism ctxt0 thms = |
431 let |
431 let |
432 val simpset = Raw_Simplifier.simpset_of (Raw_Simplifier.init_simpset thms ctxt0); |
432 val simpset = Raw_Simplifier.simpset_of (Raw_Simplifier.init_simpset thms ctxt0); |
433 val simps = map (decomp_simp ctxt0 o Thm.full_prop_of) (Raw_Simplifier.dest_simps simpset); |
433 val simps = |
|
434 map (decomp_simp ctxt0 o Thm.full_prop_of o #2) (Raw_Simplifier.dest_simps simpset); |
434 |
435 |
435 fun rewrite_term thy = Pattern.rewrite_term thy simps []; |
436 fun rewrite_term thy = Pattern.rewrite_term thy simps []; |
436 val rewrite = |
437 val rewrite = |
437 Proof_Context.init_global #> |
438 Proof_Context.init_global #> |
438 Raw_Simplifier.put_simpset simpset #> |
439 Raw_Simplifier.put_simpset simpset #> |