src/Pure/Proof/reconstruct.ML
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