--- a/Quot/Examples/LarryInt.thy	Fri Dec 11 15:58:15 2009 +0100
+++ b/Quot/Examples/LarryInt.thy	Fri Dec 11 17:03:34 2009 +0100
@@ -382,10 +382,9 @@
 
 (* PROBLEM: this has to be a definition, not an abbreviation *)
 (* otherwise the lemma nat_le_eq_zle cannot be lifted        *)
-fun
-  nat_aux
-where
-  "nat_aux (x, y) =  x - (y::nat)"
+
+abbreviation
+  "nat_aux \<equiv> \<lambda>(x, y).x - (y::nat)"
 
 quotient_def
   "nat2::int\<Rightarrow>nat"
@@ -405,12 +404,27 @@
 apply(auto)
 done
 
+ML {*
+  let
+   val parser = Args.context -- Scan.lift Args.name_source
+   fun term_pat (ctxt, str) =
+      str |> ProofContext.read_term_pattern ctxt
+          |> ML_Syntax.print_term
+          |> ML_Syntax.atomic
+in
+   ML_Antiquote.inline "term_pat" (parser >> term_pat)
+end
+
+*}
+
+consts test::"'b \<Rightarrow> 'b \<Rightarrow> 'b"
+
+
 lemma nat_le_eq_zle: "0 < w \<or> 0 \<le> z \<Longrightarrow> (nat2 w \<le> nat2 z) = (w\<le>z)"
 unfolding less_int_def
 apply(lifting nat_le_eq_zle_aux)
 apply(injection)
 apply(simp_all only: quot_respect)
 done
-(* PROBLEM *)
 
 end

--- a/Quot/QuotMain.thy	Fri Dec 11 15:58:15 2009 +0100
+++ b/Quot/QuotMain.thy	Fri Dec 11 17:03:34 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