changeset 32145 | 220c9e439d39 |
parent 32089 | 568a23753e3a |
child 32187 | cca43ca13f4f |
--- a/src/Pure/Proof/reconstruct.ML Thu Jul 23 16:43:31 2009 +0200 +++ b/src/Pure/Proof/reconstruct.ML Thu Jul 23 16:52:16 2009 +0200 @@ -255,7 +255,7 @@ let fun search env [] = error ("Unsolvable constraints:\n" ^ Pretty.string_of (Pretty.chunks (map (fn (_, p, _) => - Display_Goal.pretty_flexpair (Syntax.pp_global thy) (pairself + Display_Goal.pretty_flexpair (Syntax.init_pretty_global thy) (pairself (Envir.norm_term bigenv) p)) cs))) | search env ((u, p as (t1, t2), vs)::ps) = if u then