TFL/thry.ML
changeset 15798 016f3be5a5ec
parent 15570 8d8c70b41bab
child 16935 4d7f19d340e8
--- a/TFL/thry.ML	Thu Apr 21 19:12:03 2005 +0200
+++ b/TFL/thry.ML	Thu Apr 21 19:13:03 2005 +0200
@@ -26,17 +26,23 @@
  *    Matching
  *---------------------------------------------------------------------------*)
 
-local fun tybind (x,y) = (TVar (x, HOLogic.typeS) , y)
-      fun tmbind (x,y) = (Var  (x, Term.type_of y), y)
+local
+
+fun tybind (ixn, (S, T)) = (TVar (ixn, S), T);
+
 in
- fun match_term thry pat ob =
-    let val tsig = Sign.tsig_of (Theory.sign_of thry)
-        val (ty_theta,tm_theta) = Pattern.match tsig (pat,ob)
-    in (map tmbind tm_theta, map tybind ty_theta)
-    end
 
- fun match_type thry pat ob = map tybind (Vartab.dest
-   (Type.typ_match (Sign.tsig_of (Theory.sign_of thry)) (Vartab.empty, (pat,ob))))
+fun match_term thry pat ob =
+  let
+    val tsig = Sign.tsig_of (Theory.sign_of thry)
+    val (ty_theta, tm_theta) = Pattern.match tsig (pat,ob)
+    fun tmbind (ixn, (T, t)) = (Var (ixn, Envir.typ_subst_TVars ty_theta T), t)
+  in (map tmbind (Vartab.dest tm_theta), map tybind (Vartab.dest ty_theta))
+  end;
+
+fun match_type thry pat ob = map tybind (Vartab.dest
+  (Type.typ_match (Sign.tsig_of (Theory.sign_of thry)) (Vartab.empty, (pat, ob))));
+
 end;