equal
deleted
inserted
replaced
260 fun preprocess ctxt t = |
260 fun preprocess ctxt t = |
261 let |
261 let |
262 val thy = Proof_Context.theory_of ctxt |
262 val thy = Proof_Context.theory_of ctxt |
263 val dest = HOLogic.dest_eq o HOLogic.dest_Trueprop o Thm.prop_of |
263 val dest = HOLogic.dest_eq o HOLogic.dest_Trueprop o Thm.prop_of |
264 val rewrs = map (swap o dest) @{thms all_simps} @ |
264 val rewrs = map (swap o dest) @{thms all_simps} @ |
265 (map dest [@{thm not_ex}, @{thm not_all}, @{thm imp_conjL}]) |
265 (map dest [@{thm not_ex}, @{thm not_all}, @{thm imp_conjL}, @{thm fun_eq_iff}]) |
266 val t' = Pattern.rewrite_term thy rewrs [] (Object_Logic.atomize_term thy t) |
266 val t' = Pattern.rewrite_term thy rewrs [] (Object_Logic.atomize_term thy t) |
267 val (vs, body) = strip_all t' |
267 val (vs, body) = strip_all t' |
268 val vs' = Variable.variant_frees ctxt [t'] vs |
268 val vs' = Variable.variant_frees ctxt [t'] vs |
269 in |
269 in |
270 subst_bounds (map Free (rev vs'), body) |
270 subst_bounds (map Free (rev vs'), body) |