# HG changeset patch
# User berghofe
# Date 1275385191 -7200
# Node ID 957753a476700ff528f6f6b82c6a70d4850ff15a
# Parent  739d8b9c59da9afa2242dd5cfbaccb1fe0b10088
Renamed TypeInfer to Type_Infer.

diff -r 739d8b9c59da -r 957753a47670 src/Pure/Proof/extraction.ML
--- 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 ****)