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 20071 8f3e1ddb50e6
parent 18127 9f03d8a9a81b
child 20151 b22c14181eb7 
--- a/src/Pure/Proof/proofchecker.ML	Tue Jul 11 12:16:52 2006 +0200
+++ b/src/Pure/Proof/proofchecker.ML	Tue Jul 11 12:16:54 2006 +0200
@@ -62,7 +62,7 @@
 
       | thm_of vs Hs (Abst (s, SOME T, prf)) =
           let
-            val x = variant (names @ map fst vs) s;
+            val x = Name.variant (names @ map fst vs) s;
             val thm = thm_of ((x, T) :: vs) Hs prf
           in
             Thm.forall_intr (Thm.cterm_of sg (Free (x, T))) thm
isabelle