# HG changeset patch
# User wenzelm
# Date 1452071289 -3600
# Node ID 1add21f7cabce669c166c13f46f52d4827842293
# Parent  ea3360245939010f434ddbdc73d5b806619e3372
proper Pattern.match and corresponding Envir.subst_term, instead of Envir.norm_term of unify-family;

diff -r ea3360245939 -r 1add21f7cabc src/HOL/Eisbach/method_closure.ML
--- a/src/HOL/Eisbach/method_closure.ML	Wed Jan 06 00:04:15 2016 +0100
+++ b/src/HOL/Eisbach/method_closure.ML	Wed Jan 06 10:08:09 2016 +0100
@@ -127,14 +127,9 @@
 
 fun method_instantiate vars body ts ctxt =
   let
-    val match_types = Sign.typ_match (Proof_Context.theory_of ctxt) o apply2 Term.type_of;
-    val tyenv = fold match_types (vars ~~ ts) Vartab.empty;
-    val tenv =
-      fold (fn ((xi, T), t) => Vartab.update_new (xi, (T, t)))
-        (map Term.dest_Var vars ~~ ts) Vartab.empty;
-    val env = Envir.Envir {maxidx = ~1, tenv = tenv, tyenv = tyenv};
-
-    val morphism = Morphism.term_morphism "method_instantiate" (Envir.norm_term env);
+    val thy = Proof_Context.theory_of ctxt;
+    val subst = fold (Pattern.match thy) (vars ~~ ts) (Vartab.empty, Vartab.empty);
+    val morphism = Morphism.term_morphism "method_instantiate" (Envir.subst_term subst);
     val body' = (Method.map_source o map) (Token.transform morphism) body;
   in method_evaluate body' ctxt end;