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/HOL.thy
changeset 36330 0584e203960e
parent 36297 6b2b9516a3cd
child 36365 18bf20d0c2df 
--- a/src/HOL/HOL.thy	Sun Apr 25 22:50:47 2010 +0200
+++ b/src/HOL/HOL.thy	Sun Apr 25 23:09:32 2010 +0200
@@ -1869,7 +1869,7 @@
 proof
   assume "PROP ?ofclass"
   show "PROP ?eq"
-    by (tactic {* ALLGOALS (rtac (Drule.unconstrainTs @{thm equals_eq})) *}) 
+    by (tactic {* ALLGOALS (rtac (Thm.unconstrain_allTs @{thm equals_eq})) *}) 
       (fact `PROP ?ofclass`)
 next
   assume "PROP ?eq"
isabelle