equal
deleted
inserted
replaced
55 val substs = pattern_subtract_subst ctx vs' t t' |
55 val substs = pattern_subtract_subst ctx vs' t t' |
56 in |
56 in |
57 map (fn (vs, subst) => (vs, (v,t)::subst)) substs |
57 map (fn (vs, subst) => (vs, (v,t)::subst)) substs |
58 end |
58 end |
59 in |
59 in |
60 maps foo (inst_constrs_of (ProofContext.theory_of ctx) T) |
60 maps foo (inst_constrs_of (Proof_Context.theory_of ctx) T) |
61 end |
61 end |
62 | pattern_subtract_subst_aux vs t t' = |
62 | pattern_subtract_subst_aux vs t t' = |
63 let |
63 let |
64 val (C, ps) = strip_comb t |
64 val (C, ps) = strip_comb t |
65 val (C', qs) = strip_comb t' |
65 val (C', qs) = strip_comb t' |
74 end |
74 end |
75 |
75 |
76 (* p - q *) |
76 (* p - q *) |
77 fun pattern_subtract ctx eq2 eq1 = |
77 fun pattern_subtract ctx eq2 eq1 = |
78 let |
78 let |
79 val thy = ProofContext.theory_of ctx |
79 val thy = Proof_Context.theory_of ctx |
80 |
80 |
81 val (vs, feq1 as (_ $ (_ $ lhs1 $ _))) = dest_all_all eq1 |
81 val (vs, feq1 as (_ $ (_ $ lhs1 $ _))) = dest_all_all eq1 |
82 val (_, _ $ (_ $ lhs2 $ _)) = dest_all_all eq2 |
82 val (_, _ $ (_ $ lhs2 $ _)) = dest_all_all eq2 |
83 |
83 |
84 val substs = pattern_subtract_subst ctx vs lhs1 lhs2 |
84 val substs = pattern_subtract_subst ctx vs lhs1 lhs2 |