# HG changeset patch
# User kuncar
# Date 1332508901 -3600
# Node ID b43ddeea727f27a8ff2dc561fc71c4c1c906274f
# Parent  1a7ad2601cb53e9630ad21ac55c0646f76c71e5e
simplified code of generation of aggregate relations

diff -r 1a7ad2601cb5 -r b43ddeea727f src/HOL/Tools/Quotient/quotient_term.ML
--- a/src/HOL/Tools/Quotient/quotient_term.ML	Fri Mar 23 14:20:09 2012 +0100
+++ b/src/HOL/Tools/Quotient/quotient_term.ML	Fri Mar 23 14:21:41 2012 +0100
@@ -72,9 +72,6 @@
 
 fun defined_mapfun_data ctxt s =
   Symtab.defined (Enriched_Type.entries ctxt) s
-  
-(* makes a Free out of a TVar *)
-fun mk_Free (TVar ((x, i), _)) = Free (unprefix "'" x ^ string_of_int i, dummyT)
 
 (* looks up the (varified) rty and qty for
    a quotient definition
@@ -279,35 +276,10 @@
     SOME map_data => Const (#relmap map_data, dummyT)
   | NONE => raise LIFT_MATCH ("get_relmap (no relation map function found for type " ^ s ^ ")"))
 
-(* takes two type-environments and looks
-   up in both of them the variable v, which
-   must be listed in the environment
-*)
-fun double_lookup rtyenv qtyenv v =
-  let
-    val v' = fst (dest_TVar v)
-  in
-    (snd (the (Vartab.lookup rtyenv v')), snd (the (Vartab.lookup qtyenv v')))
-  end
-
-fun mk_relmap ctxt vs rty =
-  let
-    val vs' = map (mk_Free) vs
-
-    fun mk_relmap_aux rty =
-      case rty of
-        TVar _ => mk_Free rty
-      | Type (_, []) => HOLogic.eq_const rty
-      | Type (s, tys) => list_comb (get_relmap ctxt s, map mk_relmap_aux tys)
-      | _ => raise LIFT_MATCH ("mk_relmap (default)")
-  in
-    fold_rev Term.lambda vs' (mk_relmap_aux rty)
-  end
-
 fun get_equiv_rel thy s =
   (case Quotient_Info.lookup_quotients thy s of
     SOME qdata => #equiv_rel qdata
-  | NONE => raise LIFT_MATCH ("get_quotdata (no quotient found for type " ^ s ^ ")"))
+  | NONE => raise LIFT_MATCH ("get_equiv_rel (no quotient found for type " ^ s ^ ")"))
 
 fun equiv_match_err ctxt ty_pat ty =
   let
@@ -336,11 +308,10 @@
           end
         else
           let
-            val (rty_pat, qty_pat as Type (_, vs)) = get_rty_qty ctxt s'
-            val rtyenv = match ctxt equiv_match_err rty_pat rty
+            val (Type (_, rtys), qty_pat) = get_rty_qty ctxt s'
             val qtyenv = match ctxt equiv_match_err qty_pat qty
-            val args_aux = map (double_lookup rtyenv qtyenv) vs
-            val args = map (equiv_relation ctxt) args_aux
+            val rtys' = map (Envir.subst_type qtyenv) rtys
+            val args = map (equiv_relation ctxt) (tys ~~ rtys')
             val eqv_rel = get_equiv_rel ctxt s'
             val eqv_rel' = force_typ ctxt eqv_rel ([rty, rty] ---> @{typ bool})
           in
@@ -348,8 +319,7 @@
             then eqv_rel'
             else
               let
-                val rel_map = mk_relmap ctxt vs rty_pat
-                val result = list_comb (rel_map, args)
+                val result = list_comb (get_relmap ctxt s, args)
               in
                 mk_rel_compose (result, eqv_rel')
               end