Renamed TypeInfer to Type_Infer.

--- a/src/Pure/Proof/extraction.ML	Tue Jun 01 11:30:57 2010 +0200
+++ b/src/Pure/Proof/extraction.ML	Tue Jun 01 11:39:51 2010 +0200
@@ -166,7 +166,7 @@
       |> Proof_Syntax.strip_sorts_consttypes
       |> ProofContext.set_defsort [];
     val parse = if T = propT then Syntax.parse_prop else Syntax.parse_term;
-  in parse ctxt s |> TypeInfer.constrain T |> Syntax.check_term ctxt end;
+  in parse ctxt s |> Type_Infer.constrain T |> Syntax.check_term ctxt end;
 
 
 (**** theory data ****)