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/Old_Datatype/old_datatype.ML
changeset 60801 7664e0916eec
parent 60781 2da59cdf531c
child 61110 6b7c2ecc6aea 
--- a/src/HOL/Tools/Old_Datatype/old_datatype.ML	Mon Jul 27 16:35:12 2015 +0200
+++ b/src/HOL/Tools/Old_Datatype/old_datatype.ML	Mon Jul 27 17:44:55 2015 +0200
@@ -397,7 +397,7 @@
     (* prove  inj Rep_dt_i  and  Rep_dt_i x : rep_set_dt_i *)
 
     val fun_congs =
-      map (fn T => make_elim (Drule.instantiate' [SOME (Thm.global_ctyp_of thy5 T)] [] fun_cong)) branchTs;
+      map (fn T => make_elim (Thm.instantiate' [SOME (Thm.global_ctyp_of thy5 T)] [] fun_cong)) branchTs;
 
     fun prove_iso_thms ds (inj_thms, elem_thms) =
       let
isabelle