src/Pure/Proof/reconstruct.ML

 fun solve _ [] bigenv = bigenv
   | solve sg cs bigenv =
       let
         fun search env [] = error ("Unsolvable constraints:\n" ^
               Pretty.string_of (Pretty.chunks (map (fn (_, p, _) =>
-                Display.pretty_flexpair (Sign.pretty_term sg) (pairself
+                Display.pretty_flexpair (Sign.pp sg) (pairself
                   (Envir.norm_term bigenv) p)) cs)))
           | search env ((u, p as (t1, t2), vs)::ps) =
               if u then
                 let
                   val tn1 = Envir.norm_term bigenv t1;