equal
deleted
inserted
replaced
136 REPEAT_DETERM (FIRSTGOAL (resolve_tac monos)), |
136 REPEAT_DETERM (FIRSTGOAL (resolve_tac monos)), |
137 REPEAT_DETERM (rtac impI 1 THEN (atac 1 ORELSE tac))]) |
137 REPEAT_DETERM (rtac impI 1 THEN (atac 1 ORELSE tac))]) |
138 in Option.map prove (map_term f prop (the_default prop opt)) end; |
138 in Option.map prove (map_term f prop (the_default prop opt)) end; |
139 |
139 |
140 fun abs_params params t = |
140 fun abs_params params t = |
141 let val vs = map (Var o apfst (rpair 0)) (rename_wrt_term t params) |
141 let val vs = map (Var o apfst (rpair 0)) (Term.rename_wrt_term t params) |
142 in (list_all (params, t), (rev vs, subst_bounds (vs, t))) end; |
142 in (list_all (params, t), (rev vs, subst_bounds (vs, t))) end; |
143 |
143 |
144 fun inst_params thy (vs, p) th cts = |
144 fun inst_params thy (vs, p) th cts = |
145 let val env = Pattern.first_order_match thy (p, prop_of th) |
145 let val env = Pattern.first_order_match thy (p, prop_of th) |
146 (Vartab.empty, Vartab.empty) |
146 (Vartab.empty, Vartab.empty) |