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/Tools/BNF/bnf_def.ML
changeset 60801 7664e0916eec
parent 60784 4f590c08fd5d
child 60918 4ceef1592e8c
child 60924 610794dff23c 
--- a/src/HOL/Tools/BNF/bnf_def.ML	Mon Jul 27 16:35:12 2015 +0200
+++ b/src/HOL/Tools/BNF/bnf_def.ML	Mon Jul 27 17:44:55 2015 +0200
@@ -1251,7 +1251,7 @@
                     map Bound (live - 1 downto 0)) $ Bound live));
                 val cts = [NONE, SOME (Thm.cterm_of lthy tinst)];
               in
-                Drule.instantiate' cTs cts @{thm surj_imp_ordLeq}
+                Thm.instantiate' cTs cts @{thm surj_imp_ordLeq}
               end);
             val bd = mk_cexp
               (if live = 0 then ctwo
isabelle