Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/Pure/Proof/extraction.ML
changeset 39288 f1ae2493d93f
parent 38761 b32975d3db3e
child 39557 fe5722fce758 
--- a/src/Pure/Proof/extraction.ML	Sun Sep 12 17:39:02 2010 +0200
+++ b/src/Pure/Proof/extraction.ML	Sun Sep 12 19:04:02 2010 +0200
@@ -164,7 +164,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 |> Type_Infer.constrain T |> Syntax.check_term ctxt end;
+  in parse ctxt s |> Type.constraint T |> Syntax.check_term ctxt end;
 
 
 (**** theory data ****)
isabelle