diff -r fd6308b4df72 -r 01aa36932739 src/HOL/Import/proof_kernel.ML
--- a/src/HOL/Import/proof_kernel.ML	Thu May 27 15:28:23 2010 +0200
+++ b/src/HOL/Import/proof_kernel.ML	Thu May 27 17:41:27 2010 +0200
@@ -229,7 +229,7 @@
                 val str =
                   setmp_CRITICAL show_brackets false (G n (Syntax.string_of_term ctxt o term_of)) ct
                 val u = Syntax.parse_term ctxt str
-                  |> TypeInfer.constrain T |> Syntax.check_term ctxt
+                  |> Type_Infer.constrain T |> Syntax.check_term ctxt
             in
                 if match u
                 then quote str