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/HOL/Import/proof_kernel.ML
changeset 39288 f1ae2493d93f
parent 39236 2ec7afadc344
child 39557 fe5722fce758 
--- a/src/HOL/Import/proof_kernel.ML	Sun Sep 12 17:39:02 2010 +0200
+++ b/src/HOL/Import/proof_kernel.ML	Sun Sep 12 19:04:02 2010 +0200
@@ -222,7 +222,7 @@
                 val str =
                   G n Syntax.string_of_term (Config.put show_brackets false ctxt) (term_of ct)
                 val u = Syntax.parse_term ctxt str
-                  |> Type_Infer.constrain T |> Syntax.check_term ctxt
+                  |> Type.constraint T |> Syntax.check_term ctxt
             in
                 if match u
                 then quote str
isabelle