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/Transfer/transfer_bnf.ML
changeset 60801 7664e0916eec
parent 60728 26ffdb966759
child 61348 d7215449be83 
--- a/src/HOL/Tools/Transfer/transfer_bnf.ML	Mon Jul 27 16:35:12 2015 +0200
+++ b/src/HOL/Tools/Transfer/transfer_bnf.ML	Mon Jul 27 17:44:55 2015 +0200
@@ -359,7 +359,7 @@
         val kill_True = Local_Defs.unfold lthy [@{thm HOL.simp_thms(21)}]
       in
         thm
-        |> Drule.instantiate' cTs cts
+        |> Thm.instantiate' cTs cts
         |> Conv.fconv_rule (HOLogic.Trueprop_conv (Conv.arg_conv
           (Raw_Simplifier.rewrite lthy false @{thms eq_onp_top_eq_eq[symmetric, THEN eq_reflection]})))
         |> Local_Defs.unfold lthy eq_onps
isabelle