equal
deleted
inserted
replaced
186 Raw_Simplifier.rewrite true (get_atomize (Thm.theory_of_cterm ct)) ct; |
186 Raw_Simplifier.rewrite true (get_atomize (Thm.theory_of_cterm ct)) ct; |
187 |
187 |
188 fun atomize_prems ct = |
188 fun atomize_prems ct = |
189 if Logic.has_meta_prems (Thm.term_of ct) then |
189 if Logic.has_meta_prems (Thm.term_of ct) then |
190 Conv.params_conv ~1 (K (Conv.prems_conv ~1 atomize)) |
190 Conv.params_conv ~1 (K (Conv.prems_conv ~1 atomize)) |
191 (ProofContext.init_global (Thm.theory_of_cterm ct)) ct |
191 (Proof_Context.init_global (Thm.theory_of_cterm ct)) ct |
192 else Conv.all_conv ct; |
192 else Conv.all_conv ct; |
193 |
193 |
194 val atomize_prems_tac = CONVERSION atomize_prems; |
194 val atomize_prems_tac = CONVERSION atomize_prems; |
195 val full_atomize_tac = CONVERSION atomize; |
195 val full_atomize_tac = CONVERSION atomize; |
196 |
196 |