--- a/Quot/Examples/IntEx.thy	Mon Jan 11 01:03:34 2010 +0100
+++ b/Quot/Examples/IntEx.thy	Mon Jan 11 11:51:19 2010 +0100
@@ -199,6 +199,8 @@
 apply simp
 done
 
+
+term foldl
 lemma "foldl PLUS x [] = x"
 apply(lifting ho_tst)
 done

--- a/Quot/quotient_info.ML	Mon Jan 11 01:03:34 2010 +0100
+++ b/Quot/quotient_info.ML	Mon Jan 11 11:51:19 2010 +0100
@@ -12,6 +12,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: theory -> string -> quotdata_info     (* raises NotFound *)
+  val quotdata_lookup_type: theory -> typ -> quotdata_info   (* raises NotFound *)
   val quotdata_update_thy: string -> quotdata_info -> theory -> theory
   val quotdata_update_gen: string -> quotdata_info -> Context.generic -> Context.generic
   val print_quotinfo: Proof.context -> unit
@@ -158,8 +159,15 @@
 fun quotdata_update_thy str qinfo = QuotData.map (Symtab.update (str, qinfo))
 fun quotdata_update_gen str qinfo = Context.mapping (quotdata_update_thy str qinfo) I
 
-fun quotdata_dest thy =
-    map snd (Symtab.dest (QuotData.get thy))
+fun quotdata_lookup_type thy qty =
+  let
+    val smt = Symtab.dest (QuotData.get thy);
+    fun matches (_, x) = Sign.typ_instance thy (qty, (#qtyp x))
+  in
+    case (find_first matches smt) of
+      SOME (_, x) => x
+    | _ => raise NotFound
+  end
 
 fun print_quotinfo ctxt =
 let

--- a/Quot/quotient_term.ML	Mon Jan 11 01:03:34 2010 +0100
+++ b/Quot/quotient_term.ML	Mon Jan 11 11:51:19 2010 +0100
@@ -411,26 +411,29 @@
        end  
 
   | (_, Const _) =>
-       let 
-         fun same_name (Const (s, T)) (Const (s', T')) = (s = s') (*andalso (T = T')*)
-           | same_name _ _ = false
-          (* TODO/FIXME: This test is not enough. *) 
-          (*             Why?                     *)
-          (* Because constants can have the same name but not be the same
-             constant.  All overloaded constants have the same name but because
-             of different types they do differ.
-        
-             This code will let one write a theorem where plus on nat is
-             matched to plus on int, even if the latter is defined differently.
-    
-             This would result in hard to understand failures in injection and
-             cleaning. *)
-           (* cu: if I also test the type, then something else breaks *)
+       let
+         val thy = ProofContext.theory_of ctxt
+         fun matches_typ T T' = (
+           let
+             val rty = #rtyp (quotdata_lookup_type thy T')
+           in
+             if Sign.typ_instance thy (T, rty) then true else T = T'
+           end
+           handle Not_found => (* raised by quotdata_lookup_type *)
+             case (T, T') of
+               (TFree _, TFree _) => true
+             | (TVar _, TVar _) => true
+             | (Type (s, tys), Type (s', tys')) =>
+                 (* 'andalso' is buildin syntax so it needs to be expanded *)
+                 fold (fn x => fn y => x andalso y) (map2 matches_typ tys tys') (s = s')
+                 handle UnequalLengths => false
+         )
+         fun same_const (Const (s, T)) (Const (s', T')) = (s = s') andalso matches_typ T T'
+           | same_const _ _ = false
        in
-         if same_name rtrm qtrm then rtrm
-         else 
-           let 
-             val thy = ProofContext.theory_of ctxt
+         if same_const rtrm qtrm then rtrm
+         else
+           let
              val qtrm_str = Syntax.string_of_term ctxt qtrm
              val exc1 = LIFT_MATCH ("regularize (constant " ^ qtrm_str ^ " not found)")
              val exc2 = LIFT_MATCH ("regularize (constant " ^ qtrm_str ^ " mismatch)")