diff -r a9e55e1ef64c -r e68f501f76d0 Quot/QuotMain.thy
--- a/Quot/QuotMain.thy	Fri Dec 11 17:19:38 2009 +0100
+++ b/Quot/QuotMain.thy	Fri Dec 11 17:22:26 2009 +0100
@@ -162,31 +162,6 @@
   id_apply[THEN eq_reflection]
   id_def[THEN eq_reflection,symmetric]
 
-section {* Matching of Terms and Types *}
-
-ML {*
-fun struct_match_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 struct_match_typ (tys ~~ tys')) 
-       else false
-  | _ => false
-
-fun struct_match_term (trm, trm') = 
-   case (trm, trm') of 
-     (_, Var _) => true
-   | (Const (s, ty), Const (s', ty')) => s = s' andalso struct_match_typ (ty, ty')
-   | (Free (x, ty), Free (x', ty')) => x = x' andalso struct_match_typ (ty, ty')
-   | (Bound i, Bound j) => i = j
-   | (Abs (_, T, t), Abs (_, T', t')) => struct_match_typ (T, T') andalso struct_match_term (t, t')
-   | (t $ s, t' $ s') => struct_match_term (t, t') andalso struct_match_term (s, s') 
-   | _ => false
-*}
-
 section {* Computation of the Regularize Goal *} 
 
 (*
@@ -326,10 +301,10 @@
              val thy = ProofContext.theory_of lthy
              val rtrm' = (#rconst (qconsts_lookup thy qtrm)) handle NotFound => raise exc1
            in 
-             if struct_match_term (rtrm, rtrm') then rtrm else
+             if Pattern.matches thy (rtrm', rtrm) then rtrm else
                let
-                 val _ = tracing (Syntax.string_of_term @{context} rtrm);
-                 val _ = tracing (Syntax.string_of_term @{context} rtrm');
+                 val _ = tracing ("rtrm := " ^ Syntax.string_of_term @{context} rtrm);
+                 val _ = tracing ("rtrm':= " ^ Syntax.string_of_term @{context} rtrm');
                in raise exc2 end
            end
        end