# HG changeset patch
# User kuncar
# Date 1323436322 -3600
# Node ID b2205eb270e335b91a6d6a3be6e1ccfb0884924d
# Parent  2d894926830326e52aac27b2e16a44fcc21bfce4
context/theory parametres tuned

diff -r 2d8949268303 -r b2205eb270e3 src/HOL/Tools/Quotient/quotient_term.ML
--- a/src/HOL/Tools/Quotient/quotient_term.ML	Fri Dec 09 14:03:17 2011 +0100
+++ b/src/HOL/Tools/Quotient/quotient_term.ML	Fri Dec 09 14:12:02 2011 +0100
@@ -62,16 +62,16 @@
     AbsF => Const (@{const_name comp}, dummyT) $ trm1 $ trm2
   | RepF => Const (@{const_name comp}, dummyT) $ trm2 $ trm1
 
-fun get_mapfun_data thy s =
-  (case Symtab.lookup (Enriched_Type.entries (Proof_Context.init_global thy)) s of
+fun get_mapfun_data ctxt s =
+  (case Symtab.lookup (Enriched_Type.entries ctxt) s of
     SOME [map_data] => (case try dest_Const (#mapper map_data) of
       SOME (c, _) => (Const (c, dummyT), #variances map_data)
     | NONE => raise LIFT_MATCH ("map function for type " ^ quote s ^ " is not a constant."))
   | SOME _ => raise LIFT_MATCH ("map function for type " ^ quote s ^ " is non-singleton entry.")
   | NONE => raise LIFT_MATCH ("No map function for type " ^ quote s ^ " found.")) 
 
-fun defined_mapfun_data thy s =
-  Symtab.defined (Enriched_Type.entries (Proof_Context.init_global thy)) s
+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)
@@ -79,10 +79,14 @@
 (* looks up the (varified) rty and qty for
    a quotient definition
 *)
-fun get_rty_qty thy s =
-  (case Quotient_Info.lookup_quotients_global thy s of
-    SOME qdata => (#rtyp qdata, #qtyp qdata)
-  | NONE => raise LIFT_MATCH ("No quotient type " ^ quote s ^ " found."))
+fun get_rty_qty ctxt s =
+  let
+    val thy = Proof_Context.theory_of ctxt
+  in
+    (case Quotient_Info.lookup_quotients_global thy s of
+      SOME qdata => (#rtyp qdata, #qtyp qdata)
+    | NONE => raise LIFT_MATCH ("No quotient type " ^ quote s ^ " found."))
+  end
 
 (* matches a type pattern with a type *)
 fun match ctxt err ty_pat ty =
@@ -168,7 +172,6 @@
 
 fun absrep_fun flag ctxt (rty, qty) =
   let
-    val thy = Proof_Context.theory_of ctxt
     fun absrep_args tys tys' variances =
       let
         fun absrep_arg (types, (_, variant)) =
@@ -199,18 +202,18 @@
           if s = s'
           then
             let
-              val (map_fun, variances) = get_mapfun_data thy s
+              val (map_fun, variances) = get_mapfun_data ctxt s
               val args = absrep_args tys tys' variances
             in
               list_comb (map_fun, args)
             end
           else
             let
-              val (Type (_, rtys), qty_pat) = get_rty_qty thy s'
+              val (Type (_, rtys), qty_pat) = get_rty_qty ctxt s'
               val qtyenv = match ctxt absrep_match_err qty_pat qty
               val rtys' = map (Envir.subst_type qtyenv) rtys
             in
-              if not (defined_mapfun_data thy s)
+              if not (defined_mapfun_data ctxt s)
               then
                 (*
                     If we don't know a map function for the raw type,
@@ -221,7 +224,7 @@
                 test_identities tys rtys' s s'
               else
                 let
-                  val (map_fun, variances) = get_mapfun_data thy s
+                  val (map_fun, variances) = get_mapfun_data ctxt s
                   val args = absrep_args tys rtys' variances
                 in
                   if forall is_identity args
@@ -320,43 +323,40 @@
    that will be the argument of Respects
 *)
 fun equiv_relation ctxt (rty, qty) =
-  let
-    val thy = Proof_Context.theory_of ctxt
-  in
-    if rty = qty
-    then HOLogic.eq_const rty
-    else
-      case (rty, qty) of
-        (Type (s, tys), Type (s', tys')) =>
-          if s = s'
-          then
-            let
-              val args = map (equiv_relation ctxt) (tys ~~ tys')
-            in
-              list_comb (get_relmap ctxt s, args)
-            end
-          else
-            let
-              val (rty_pat, qty_pat as Type (_, vs)) = get_rty_qty thy s'
-              val rtyenv = match ctxt equiv_match_err rty_pat rty
-              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 eqv_rel = get_equiv_rel ctxt s'
-              val eqv_rel' = force_typ ctxt eqv_rel ([rty, rty] ---> @{typ bool})
-            in
-              if forall is_eq args
-              then eqv_rel'
-              else
-                let
-                  val rel_map = mk_relmap ctxt vs rty_pat
-                  val result = list_comb (rel_map, args)
-                in
-                  mk_rel_compose (result, eqv_rel')
-                end
-            end
-      | _ => HOLogic.eq_const rty
-  end
+  if rty = qty
+  then HOLogic.eq_const rty
+  else
+    case (rty, qty) of
+      (Type (s, tys), Type (s', tys')) =>
+        if s = s'
+        then
+          let
+            val args = map (equiv_relation ctxt) (tys ~~ tys')
+          in
+            list_comb (get_relmap ctxt s, args)
+          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 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 eqv_rel = get_equiv_rel ctxt s'
+            val eqv_rel' = force_typ ctxt eqv_rel ([rty, rty] ---> @{typ bool})
+          in
+            if forall is_eq args
+            then eqv_rel'
+            else
+              let
+                val rel_map = mk_relmap ctxt vs rty_pat
+                val result = list_comb (rel_map, args)
+              in
+                mk_rel_compose (result, eqv_rel')
+              end
+          end
+    | _ => HOLogic.eq_const rty
+
 
 fun equiv_relation_chk ctxt (rty, qty) =
   equiv_relation ctxt (rty, qty)