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 37145 01aa36932739
parent 36960 01594f816e3a
child 37146 f652333bbf8e 
--- a/src/HOL/Import/proof_kernel.ML	Thu May 27 15:28:23 2010 +0200
+++ b/src/HOL/Import/proof_kernel.ML	Thu May 27 17:41:27 2010 +0200
@@ -229,7 +229,7 @@
                 val str =
                   setmp_CRITICAL show_brackets false (G n (Syntax.string_of_term ctxt o term_of)) ct
                 val u = Syntax.parse_term ctxt str
-                  |> TypeInfer.constrain T |> Syntax.check_term ctxt
+                  |> Type_Infer.constrain T |> Syntax.check_term ctxt
             in
                 if match u
                 then quote str
isabelle