--- a/src/HOL/Tools/Lifting/lifting_info.ML Fri Sep 20 16:32:27 2013 +0200
+++ b/src/HOL/Tools/Lifting/lifting_info.ML Fri Sep 20 17:08:08 2013 +0200
@@ -70,7 +70,7 @@
{quot_thm = quot_thm2, pcr_info = pcr_info2}) =
Thm.eq_thm (quot_thm1, quot_thm2) andalso option_eq pcr_eq (pcr_info1, pcr_info2)
-fun join_restore_data key (rd1, rd2) =
+fun join_restore_data key (rd1:restore_data, rd2) =
if pointer_eq (rd1, rd2) then raise Symtab.SAME else
if not (quotient_eq (#quotient rd1, #quotient rd2)) then raise Symtab.DUP key else
{ quotient = #quotient rd1,
--- a/src/HOL/Tools/Lifting/lifting_setup.ML Fri Sep 20 16:32:27 2013 +0200
+++ b/src/HOL/Tools/Lifting/lifting_setup.ML Fri Sep 20 17:08:08 2013 +0200
@@ -925,7 +925,7 @@
type restore_data = {quotient : Lifting_Info.quotient, transfer_rules: thm Item_Net.T}
-fun get_transfer_rel qinfo =
+fun get_transfer_rel (qinfo : Lifting_Info.quotient) =
let
fun get_pcrel pcr_def = pcr_def |> concl_of |> Logic.dest_equals |> fst |> head_of
in
@@ -954,10 +954,7 @@
let
fun get_transfer_rules_to_delete qinfo ctxt =
let
- fun get_pcrel pcr_def = pcr_def |> concl_of |> Logic.dest_equals |> fst |> head_of
- val transfer_rel = if is_some (#pcr_info qinfo)
- then get_pcrel (#pcrel_def (the (#pcr_info qinfo)))
- else quot_thm_crel (#quot_thm qinfo)
+ val transfer_rel = get_transfer_rel qinfo
in
filter_transfer_rules_by_rel transfer_rel (Transfer.get_transfer_raw ctxt)
end
@@ -990,7 +987,7 @@
fun update_transfer_rules pointer lthy =
let
- fun new_transfer_rules { quotient = qinfo, ... } lthy =
+ fun new_transfer_rules ({ quotient = qinfo, ... }:Lifting_Info.restore_data) lthy =
let
val transfer_rel = get_transfer_rel qinfo
val transfer_rules = filter_transfer_rules_by_rel transfer_rel (Transfer.get_transfer_raw lthy)