src/Pure/Proof/extraction.ML
changeset 39288 f1ae2493d93f
parent 38761 b32975d3db3e
child 39557 fe5722fce758
     1.1 --- a/src/Pure/Proof/extraction.ML	Sun Sep 12 17:39:02 2010 +0200
     1.2 +++ b/src/Pure/Proof/extraction.ML	Sun Sep 12 19:04:02 2010 +0200
     1.3 @@ -164,7 +164,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 |> Type_Infer.constrain T |> Syntax.check_term ctxt end;
     1.8 +  in parse ctxt s |> Type.constraint T |> Syntax.check_term ctxt end;
     1.9  
    1.10  
    1.11  (**** theory data ****)