# HG changeset patch
# User kuncar
# Date 1430567886 -7200
# Node ID 29ac1c6a1fbbf4a320b78041da2e08a4f241dfee
# Parent  0daab758e087f223d2f56c1a64c0a813c04c83e3
equivalence in code_dt data structure must respect both rty and qty

diff -r 0daab758e087 -r 29ac1c6a1fbb src/HOL/Tools/Lifting/lifting_def_code_dt.ML
--- a/src/HOL/Tools/Lifting/lifting_def_code_dt.ML	Sat May 02 13:58:06 2015 +0200
+++ b/src/HOL/Tools/Lifting/lifting_def_code_dt.ML	Sat May 02 13:58:06 2015 +0200
@@ -67,14 +67,15 @@
 fun wit_of_code_dt (CODE_DT code_dt) = #wit code_dt;
 fun wit_thm_of_code_dt (CODE_DT code_dt) = #wit_thm code_dt;
 fun rep_isom_data_of_code_dt (CODE_DT code_dt) = #rep_isom_data code_dt;
-fun rty_equiv (T, U) = Type.raw_instance (T, U) andalso Type.raw_instance (U, T);
-val code_dt_eq = rty_equiv o apply2 rty_of_code_dt;
+fun ty_alpha_equiv (T, U) = Type.raw_instance (T, U) andalso Type.raw_instance (U, T);
+fun code_dt_eq c = (ty_alpha_equiv o apply2 rty_of_code_dt) c 
+  andalso (ty_alpha_equiv o apply2 qty_of_code_dt) c;
 fun term_of_code_dt code_dt = code_dt |> `rty_of_code_dt ||> qty_of_code_dt |> HOLogic.mk_prodT
   |> Net.encode_type |> single;
 
 (* modulo renaming, typ must contain TVars *)
 fun is_code_dt_of_type (rty, qty) code_dt = code_dt |> `rty_of_code_dt ||> qty_of_code_dt
-  |> HOLogic.mk_prodT |> curry rty_equiv (HOLogic.mk_prodT (rty, qty));
+  |> HOLogic.mk_prodT |> curry ty_alpha_equiv (HOLogic.mk_prodT (rty, qty));
 
 fun mk_rep_isom_data isom transfer bundle_name pointer =
   REP_ISOM { isom = isom, transfer = transfer, bundle_name = bundle_name, pointer = pointer}