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/proofchecker.ML
changeset 36042 85efdadee8ae
parent 35985 0bbf0d2348f9
child 37229 47eb565796f4 
--- a/src/Pure/Proof/proofchecker.ML	Tue Mar 30 12:47:39 2010 +0200
+++ b/src/Pure/Proof/proofchecker.ML	Tue Mar 30 15:25:30 2010 +0200
@@ -35,7 +35,7 @@
 
     fun thm_of_atom thm Ts =
       let
-        val tvars = OldTerm.term_tvars (Thm.full_prop_of thm);
+        val tvars = Term.add_tvars (Thm.full_prop_of thm) [] |> rev;
         val (fmap, thm') = Thm.varifyT_global' [] thm;
         val ctye = map (pairself (Thm.ctyp_of thy))
           (map TVar tvars @ map (fn ((_, S), ixn) => TVar (ixn, S)) fmap ~~ Ts)
isabelle