130 fun add_cnstrt Ts prop prf cs env vTs (t, u) = |
130 fun add_cnstrt Ts prop prf cs env vTs (t, u) = |
131 let |
131 let |
132 val t' = mk_abs Ts t; |
132 val t' = mk_abs Ts t; |
133 val u' = mk_abs Ts u |
133 val u' = mk_abs Ts u |
134 in |
134 in |
135 (prop, prf, cs, Pattern.unify (sg, env, [(t', u')]), vTs) |
135 (prop, prf, cs, Pattern.unify sg (t', u') env, vTs) |
136 handle Pattern.Pattern => |
136 handle Pattern.Pattern => |
137 let val (env', cs') = decompose sg [] (env, (t', u')) |
137 let val (env', cs') = decompose sg [] (env, (t', u')) |
138 in (prop, prf, cs @ cs', env', vTs) end |
138 in (prop, prf, cs @ cs', env', vTs) end |
139 | Pattern.Unif => |
139 | Pattern.Unif => |
140 cantunify sg (Envir.norm_term env t', Envir.norm_term env u') |
140 cantunify sg (Envir.norm_term env t', Envir.norm_term env u') |
266 let |
266 let |
267 val tn1 = Envir.norm_term bigenv t1; |
267 val tn1 = Envir.norm_term bigenv t1; |
268 val tn2 = Envir.norm_term bigenv t2 |
268 val tn2 = Envir.norm_term bigenv t2 |
269 in |
269 in |
270 if Pattern.pattern tn1 andalso Pattern.pattern tn2 then |
270 if Pattern.pattern tn1 andalso Pattern.pattern tn2 then |
271 ((Pattern.unify (sg, env, [(tn1, tn2)]), ps) handle Pattern.Unif => |
271 (Pattern.unify sg (tn1, tn2) env, ps) handle Pattern.Unif => |
272 cantunify sg (tn1, tn2)) |
272 cantunify sg (tn1, tn2) |
273 else |
273 else |
274 let val (env', cs') = decompose sg [] (env, (tn1, tn2)) |
274 let val (env', cs') = decompose sg [] (env, (tn1, tn2)) |
275 in if cs' = [(tn1, tn2)] then |
275 in if cs' = [(tn1, tn2)] then |
276 apsnd (cons (false, (tn1, tn2), vs)) (search env ps) |
276 apsnd (cons (false, (tn1, tn2), vs)) (search env ps) |
277 else search env' (map (fn q => (true, q, vs)) cs' @ ps) |
277 else search env' (map (fn q => (true, q, vs)) cs' @ ps) |