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