--- a/src/HOL/Tools/Lifting/lifting_bnf.ML Fri Mar 06 14:01:08 2015 +0100
+++ b/src/HOL/Tools/Lifting/lifting_bnf.ML Fri Mar 06 15:58:56 2015 +0100
@@ -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 (Proof_Context.cterm_of ctxt))) vars UNIVs
+ val inst = map2 (curry (apply2 (Thm.cterm_of ctxt))) vars 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)