equal
deleted
inserted
replaced
263 fun solve _ [] bigenv = bigenv |
263 fun solve _ [] bigenv = bigenv |
264 | solve sg cs bigenv = |
264 | solve sg cs bigenv = |
265 let |
265 let |
266 fun search env [] = error ("Unsolvable constraints:\n" ^ |
266 fun search env [] = error ("Unsolvable constraints:\n" ^ |
267 Pretty.string_of (Pretty.chunks (map (fn (_, p, _) => |
267 Pretty.string_of (Pretty.chunks (map (fn (_, p, _) => |
268 Display.pretty_flexpair (Sign.pretty_term sg) (pairself |
268 Display.pretty_flexpair (Sign.pp sg) (pairself |
269 (Envir.norm_term bigenv) p)) cs))) |
269 (Envir.norm_term bigenv) p)) cs))) |
270 | search env ((u, p as (t1, t2), vs)::ps) = |
270 | search env ((u, p as (t1, t2), vs)::ps) = |
271 if u then |
271 if u then |
272 let |
272 let |
273 val tn1 = Envir.norm_term bigenv t1; |
273 val tn1 = Envir.norm_term bigenv t1; |