# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1263026314 -3600
# Node ID b3bb2bad952f6220c5fbdd02eb406fbbfffa7e3c
# Parent  224909b9399f20d2db6ebe27eea59b19c3bacc55
introduced separate match function

diff -r 224909b9399f -r b3bb2bad952f Quot/quotient_term.ML
--- a/Quot/quotient_term.ML	Sat Jan 09 08:52:06 2010 +0100
+++ b/Quot/quotient_term.ML	Sat Jan 09 09:38:34 2010 +0100
@@ -98,6 +98,15 @@
   (snd (the (Vartab.lookup rtyenv v')), snd (the (Vartab.lookup qtyenv v')))
 end
 
+(* matches a type pattern with a type *)
+fun match ctxt err ty_pat ty =
+let
+  val thy = ProofContext.theory_of ctxt
+in
+  Sign.typ_match thy (ty_pat, ty) Vartab.empty
+  handle MATCH_TYPE => err ctxt ty_pat ty
+end
+
 (* produces the rep or abs constant for a qty *)
 fun absrep_const flag ctxt qty_str =
 let
@@ -170,15 +179,12 @@
              val args = map (absrep_fun flag ctxt) (tys ~~ tys')
            in
              list_comb (get_mapfun ctxt s, args)
-           end
+           end 
         else
            let
-             val thy = ProofContext.theory_of ctxt
              val (rty_pat, qty_pat as Type (_, vs)) = get_rty_qty ctxt s'
-             val rtyenv = Sign.typ_match thy (rty_pat, rty) Vartab.empty
-                          handle MATCH_TYPE => absrep_match_err ctxt rty_pat rty
-             val qtyenv = Sign.typ_match thy (qty_pat, qty) Vartab.empty
-                          handle MATCH_TYPE => absrep_match_err ctxt qty_pat qty 
+             val rtyenv = match ctxt absrep_match_err rty_pat rty
+             val qtyenv = match ctxt absrep_match_err qty_pat qty
              val args_aux = map (double_lookup rtyenv qtyenv) vs 
              val args = map (absrep_fun flag ctxt) args_aux
              val map_fun = mk_mapfun ctxt vs rty_pat       
@@ -275,12 +281,9 @@
          end  
        else 
          let
-           val thy = ProofContext.theory_of ctxt
            val (rty_pat, qty_pat as Type (_, vs)) = get_rty_qty ctxt s'
-           val rtyenv = Sign.typ_match thy (rty_pat, rty) Vartab.empty
-                        handle MATCH_TYPE => equiv_match_err ctxt rty_pat rty
-           val qtyenv = Sign.typ_match thy (qty_pat, qty) Vartab.empty
-                        handle MATCH_TYPE => equiv_match_err ctxt qty_pat qty 
+           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 rel_map = mk_relmap ctxt vs rty_pat