--- a/src/HOL/Tools/Lifting/lifting_bnf.ML Fri Jul 03 16:19:45 2015 +0200
+++ b/src/HOL/Tools/Lifting/lifting_bnf.ML Sun Jul 05 15:02:30 2015 +0200
@@ -23,7 +23,7 @@
fun get_lhs thm = thm |> Thm.concl_of |> HOLogic.dest_Trueprop |> HOLogic.dest_eq |> fst
val vars = get_lhs rel_Grp |> strip_comb |> snd |> map_filter (try (strip_comb #> snd #> hd))
val UNIVs = map (fn var => HOLogic.mk_UNIV (var |> dest_Var |> snd |> dest_Type |> snd |> hd)) vars
- val inst = map2 (curry (apply2 (Thm.cterm_of ctxt))) vars UNIVs
+ val inst = map dest_Var vars ~~ map (Thm.cterm_of ctxt) UNIVs
val rel_Grp_UNIV_sym = rel_Grp |> Drule.instantiate_normalize ([], inst)
|> Local_Defs.unfold ctxt @{thms subset_UNIV[THEN eqTrueI] UNIV_def[symmetric] simp_thms(21)}
|> (fn thm => thm RS sym)