author | berghofe |
Tue, 01 Jun 2010 11:39:51 +0200 | |
changeset 37237 | 957753a47670 |
parent 37236 | 739d8b9c59da |
child 37238 | d94459cf7ea8 |
--- 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 ****)