# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1259086169 -3600
# Node ID 98dbe4fe6afefbf456b475768c7cca370359d954
# Parent  321d6c561575ae009d5c63f99312419fa45e0309
changed unification to matching

diff -r 321d6c561575 -r 98dbe4fe6afe QuotMain.thy
--- a/QuotMain.thy	Tue Nov 24 18:13:57 2009 +0100
+++ b/QuotMain.thy	Tue Nov 24 19:09:29 2009 +0100
@@ -1592,6 +1592,18 @@
   THEN' (quotient_tac quot);
 *}
 
+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
+*}
+
 ML {* 
 fun prep_trm thy (x, (T, t)) = 
   (cterm_of thy (Var (x, T)), cterm_of thy t) 
@@ -1601,10 +1613,9 @@
 *}
 
 ML {*
-fun unify_prs thy pat trm = 
+fun matching_prs thy pat trm = 
 let
-  val init = Envir.empty 0 (* FIXME: get the max-index *)
-  val univ = Unify.smash_unifiers thy [(pat, trm)] init
+  val univ = Unify.matchers thy [(pat, trm)] 
   val SOME (env, _) = Seq.pull univ
   val tenv = Vartab.dest (Envir.term_env env)
   val tyenv =  Vartab.dest (Envir.type_env env)
@@ -1613,7 +1624,6 @@
 end 
 *}
 
-
 ML {*
 fun lambda_prs_tac lthy quot =
   (EqSubst.eqsubst_tac lthy [0] @{thms LAMBDA_PRS}