equal
deleted
inserted
replaced
253 fun solve _ [] bigenv = bigenv |
253 fun solve _ [] bigenv = bigenv |
254 | solve thy cs bigenv = |
254 | solve thy cs bigenv = |
255 let |
255 let |
256 fun search env [] = error ("Unsolvable constraints:\n" ^ |
256 fun search env [] = error ("Unsolvable constraints:\n" ^ |
257 Pretty.string_of (Pretty.chunks (map (fn (_, p, _) => |
257 Pretty.string_of (Pretty.chunks (map (fn (_, p, _) => |
258 Display_Goal.pretty_flexpair (Syntax.pp_global thy) (pairself |
258 Display_Goal.pretty_flexpair (Syntax.init_pretty_global thy) (pairself |
259 (Envir.norm_term bigenv) p)) cs))) |
259 (Envir.norm_term bigenv) p)) cs))) |
260 | search env ((u, p as (t1, t2), vs)::ps) = |
260 | search env ((u, p as (t1, t2), vs)::ps) = |
261 if u then |
261 if u then |
262 let |
262 let |
263 val tn1 = Envir.norm_term bigenv t1; |
263 val tn1 = Envir.norm_term bigenv t1; |