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