# HG changeset patch
# User kuncar
# Date 1379689688 -7200
# Node ID 124bb918f45f756d1339c2f68e7cca8535cca8a8
# Parent  ae7f50e70c09e1d82378da1f0c42c43a65fcbbe5
make SML/NJ happy

diff -r ae7f50e70c09 -r 124bb918f45f src/HOL/Tools/Lifting/lifting_info.ML
--- 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, 
diff -r ae7f50e70c09 -r 124bb918f45f src/HOL/Tools/Lifting/lifting_setup.ML
--- 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)