--- a/QuotMain.thy	Fri Dec 04 18:32:19 2009 +0100
+++ b/QuotMain.thy	Fri Dec 04 21:42:55 2009 +0100
@@ -351,6 +351,30 @@
 *}
 
 ML {*
+fun matches_typ (ty, ty') =
+  case (ty, ty') of
+    (_, TVar _) => true
+  | (TFree x, TFree x') => x = x'
+  | (Type (s, tys), Type (s', tys')) => 
+       s = s' andalso 
+       if (length tys = length tys') 
+       then (List.all matches_typ (tys ~~ tys')) 
+       else false
+  | _ => false
+*}
+ML {*
+fun matches_term (trm, trm') = 
+   case (trm, trm') of 
+     (_, Var _) => true
+   | (Const (s, ty), Const (s', ty')) => s = s' andalso matches_typ (ty, ty')
+   | (Free (x, ty), Free (x', ty')) => x = x' andalso matches_typ (ty, ty')
+   | (Bound i, Bound j) => i = j
+   | (Abs (_, T, t), Abs (_, T', t')) => matches_typ (T, T') andalso matches_term (t, t')
+   | (t $ s, t' $ s') => matches_term (t, t') andalso matches_term (s, s') 
+   | _ => false
+*}
+
+ML {*
 val mk_babs = Const (@{const_name Babs}, dummyT)
 val mk_ball = Const (@{const_name Ball}, dummyT)
 val mk_bex  = Const (@{const_name Bex}, dummyT)
@@ -388,6 +412,7 @@
          then Abs (x, ty, subtrm)
          else mk_babs $ (mk_resp $ mk_resp_arg lthy (ty, ty')) $ subtrm
        end
+
   | (Const (@{const_name "All"}, ty) $ t, Const (@{const_name "All"}, ty') $ t') =>
        let
          val subtrm = apply_subt (regularize_trm lthy) t t'
@@ -396,6 +421,7 @@
          then Const (@{const_name "All"}, ty) $ subtrm
          else mk_ball $ (mk_resp $ mk_resp_arg lthy (qnt_typ ty, qnt_typ ty')) $ subtrm
        end
+
   | (Const (@{const_name "Ex"}, ty) $ t, Const (@{const_name "Ex"}, ty') $ t') =>
        let
          val subtrm = apply_subt (regularize_trm lthy) t t'
@@ -404,30 +430,59 @@
          then Const (@{const_name "Ex"}, ty) $ subtrm
          else mk_bex $ (mk_resp $ mk_resp_arg lthy (qnt_typ ty, qnt_typ ty')) $ subtrm
        end
-    (* FIXME: Should = only be replaced, when fully applied? *) 
-    (* Then there must be a 2nd argument                     *)
-  | (Const (@{const_name "op ="}, ty) $ t, Const (@{const_name "op ="}, ty') $ t') =>
-       let
-         val subtrm = regularize_trm lthy t t'
+
+  | (* equalities need to be replaced by appropriate equivalence relations *) 
+    (Const (@{const_name "op ="}, ty), Const (@{const_name "op ="}, ty')) =>
+         if ty = ty'
+         then rtrm
+         else mk_resp_arg lthy (domain_type ty, domain_type ty') 
+
+  | (* in this case we check whether the given equivalence relation is correct *) 
+    (rel, Const (@{const_name "op ="}, ty')) =>
+       let 
+         val exc = LIFT_MATCH "regularise (relation mismatch)"
+         val rel_ty = (fastype_of rel) handle TERM _ => raise exc 
+         val rel' = mk_resp_arg lthy (domain_type rel_ty, domain_type ty') 
+       in 
+         if rel' = rel
+         then rtrm
+         else raise exc
+       end  
+  | (_, Const (s, _)) =>
+       let 
+         fun same_name (Const (s, _)) (Const (s', _)) = (s = s')
+           | same_name _ _ = false
        in
-         if ty = ty'
-         then Const (@{const_name "op ="}, ty) $ subtrm
-         else mk_resp_arg lthy (domain_type ty, domain_type ty') $ subtrm
+         if same_name rtrm qtrm 
+         then rtrm 
+         else 
+           let 
+             fun exc1 s = LIFT_MATCH ("regularize (constant " ^ s ^ " not found)")
+             val exc2   = LIFT_MATCH ("regularize (constant mismatch)")
+             val thy = ProofContext.theory_of lthy
+             val rtrm' = (#rconst (qconsts_lookup thy s)) handle NotFound => raise (exc1 s) 
+           in 
+             if matches_term (rtrm, rtrm')
+             then rtrm
+             else raise exc2
+           end
        end 
+
   | (t1 $ t2, t1' $ t2') =>
        (regularize_trm lthy t1 t1') $ (regularize_trm lthy t2 t2')
+
   | (Free (x, ty), Free (x', ty')) => 
        (* this case cannot arrise as we start with two fully atomized terms *)
        raise (LIFT_MATCH "regularize (frees)")
+
   | (Bound i, Bound i') =>
        if i = i' 
        then rtrm 
-       else raise (LIFT_MATCH "regularize (bounds)")
-  | (Const (s, ty), Const (s', ty')) =>
-       if s = s' andalso ty = ty'
-       then rtrm
-       else rtrm (* FIXME: check correspondence according to definitions *) 
-  | (rt, qt) => 
+       else raise (LIFT_MATCH "regularize (bounds mismatch)")
+
+  
+
+  | (rt, qt) =>
        raise (LIFT_MATCH "regularize (default)")
 *}
 
@@ -690,10 +745,10 @@
         val rargs' = map (inj_repabs_trm lthy) (rargs ~~ qargs)
       in
         case (rhead, qhead) of
-          (Const _, Const _) =>
-             if rty = qty                   
+          (Const (s, T), Const (s', T')) =>
+             if T = T'                    
              then list_comb (rhead, rargs') 
-             else mk_repabs lthy (rty, qty) (list_comb (rhead, rargs')) 
+             else list_comb (mk_repabs lthy (T, T') rhead, rargs') 
         | (Free (x, T), Free (x', T')) => 
              if T = T' 
              then list_comb (rhead, rargs')