# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1263479124 -3600
# Node ID cc951743c5e2df54fd50e10d03b1449e16de25ba
# Parent  ab8a58973861063b77dce426ff809de792e98c16
Simplified matches_typ.

diff -r ab8a58973861 -r cc951743c5e2 Quot/Examples/IntEx.thy
--- a/Quot/Examples/IntEx.thy	Thu Jan 14 12:23:59 2010 +0100
+++ b/Quot/Examples/IntEx.thy	Thu Jan 14 15:25:24 2010 +0100
@@ -13,15 +13,6 @@
   apply(auto simp add: mem_def expand_fun_eq)
   done
 
-thm quot_equiv
-
-thm quot_thm
-
-thm my_int_equivp
-
-print_theorems
-print_quotients
-
 quotient_definition
   "ZERO :: my_int"
 as
diff -r ab8a58973861 -r cc951743c5e2 Quot/quotient_info.ML
--- a/Quot/quotient_info.ML	Thu Jan 14 12:23:59 2010 +0100
+++ b/Quot/quotient_info.ML	Thu Jan 14 15:25:24 2010 +0100
@@ -11,6 +11,7 @@
 
   type quotdata_info = {qtyp: typ, rtyp: typ, equiv_rel: term, equiv_thm: thm}
   val transform_quotdata: morphism -> quotdata_info -> quotdata_info
+  val quotdata_lookup_raw: theory -> string -> quotdata_info option
   val quotdata_lookup: theory -> string -> quotdata_info     (* raises NotFound *)
   val quotdata_update_thy: string -> quotdata_info -> theory -> theory
   val quotdata_update_gen: string -> quotdata_info -> Context.generic -> Context.generic
@@ -147,7 +148,9 @@
      equiv_rel = Morphism.term phi equiv_rel,
      equiv_thm = Morphism.thm phi equiv_thm}
 
-fun quotdata_lookup thy str = 
+fun quotdata_lookup_raw thy str = Symtab.lookup (QuotData.get thy) str
+
+fun quotdata_lookup thy str =
   case Symtab.lookup (QuotData.get thy) str of
     SOME qinfo => qinfo
   | NONE => raise NotFound
diff -r ab8a58973861 -r cc951743c5e2 Quot/quotient_term.ML
--- a/Quot/quotient_term.ML	Thu Jan 14 12:23:59 2010 +0100
+++ b/Quot/quotient_term.ML	Thu Jan 14 15:25:24 2010 +0100
@@ -389,22 +389,17 @@
 
 (* Checks that two types match, for example:
      rty -> rty   matches   qty -> qty *)
-fun matches_typ thy T T' =
-  case (T, T') of
-    (TFree _, TFree _) => true
-  | (TVar _, TVar _) => true
-  | (Type (s, tys), Type (s', tys')) => (
-      if T = T' then true else
-      let
-        val rty = #rtyp (Quotient_Info.quotdata_lookup thy s')
-      in
-        if Sign.typ_instance thy (T, rty) then true else false
-      end
-      handle Not_found =>
-        if length tys <> length tys' then false else
-        (* 'andalso' is buildin syntax so it needs to be expanded *)
-        fold (fn x => fn y => x andalso y) (map2 (matches_typ thy) tys tys') (s = s')
-      )
+fun matches_typ thy rT qT =
+  if rT = qT then true else
+  case (rT, qT) of
+    (Type (rs, rtys), Type (qs, qtys)) =>
+      if rs = qs then
+        if length rtys <> length qtys then false else
+        forall (fn x => x = true) (map2 (matches_typ thy) rtys qtys)
+      else
+        (case Quotient_Info.quotdata_lookup_raw thy qs of
+          SOME quotinfo => Sign.typ_instance thy (rT, #rtyp quotinfo)
+        | NONE => false)
   | _ => false