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