--- a/QuotMain.thy	Sat Dec 05 22:38:42 2009 +0100
+++ b/QuotMain.thy	Sun Dec 06 00:13:35 2009 +0100
@@ -740,12 +740,17 @@
         then rtrm 
         else mk_repabs lthy (T, T') rtrm
 
-  | (Const (_, T), Const (_, T')) =>
-        if T = T'                    
+  | (_, Const (@{const_name "op ="}, _)) => rtrm
+
+    (* FIXME: check here that rtrm is the corresponding definition for teh const *)
+  | (_, Const (_, T')) =>
+      let
+        val rty = fastype_of rtrm
+      in 
+        if rty = T'                    
         then rtrm
-        else mk_repabs lthy (T, T') rtrm
-  
-  | (_, Const (@{const_name "op ="}, _)) => rtrm
+        else mk_repabs lthy (rty, T') rtrm
+      end   
   
   | _ => raise (LIFT_MATCH "injection")
 *}
@@ -773,6 +778,12 @@
      resolve_tac (quotient_rules_get ctxt)])
 *}
 
+(* solver for the simplifier *)
+ML {*
+fun quotient_solver_tac ss = quotient_tac (Simplifier.the_context ss)
+val quotient_solver = Simplifier.mk_solver' "Quotient goal solver" quotient_solver_tac
+*}
+
 definition
   "QUOT_TRUE x \<equiv> True"
 
@@ -1096,11 +1107,6 @@
 *)
 
 ML {*
-fun quotient_solver_tac ss = quotient_tac (Simplifier.the_context ss)
-val quotient_solver = Simplifier.mk_solver' "Quotient goal solver" quotient_solver_tac
-*}
-
-ML {*
 fun clean_tac lthy =
   let
     val thy = ProofContext.theory_of lthy;