expand_atom: Type.raw_match;

--- a/src/Pure/Isar/proof_context.ML	Thu Apr 13 12:00:59 2006 +0200
+++ b/src/Pure/Isar/proof_context.ML	Thu Apr 13 12:01:00 2006 +0200
@@ -508,7 +508,7 @@
 
     fun expand_var (xi, T) =
       (case Vartab.lookup binds xi of
-        SOME t => Envir.expand_atom (tsig_of ctxt) T t
+        SOME t => Envir.expand_atom T t
       | NONE =>
           if schematic then Var (xi, T)
           else error ("Unbound schematic variable: " ^ Syntax.string_of_vname xi));

--- a/src/Pure/envir.ML	Thu Apr 13 12:00:59 2006 +0200
+++ b/src/Pure/envir.ML	Thu Apr 13 12:01:00 2006 +0200
@@ -38,7 +38,7 @@
   val subst_TVars: Type.tyenv -> term -> term
   val subst_Vars: tenv -> term -> term
   val subst_vars: Type.tyenv * tenv -> term -> term
-  val expand_atom: Type.tsig -> typ -> typ * term -> term
+  val expand_atom: typ -> typ * term -> term
 end;
 
 structure Envir : ENVIR =
@@ -297,8 +297,8 @@
 
 (* expand_atom *)
 
-fun expand_atom tsig T (U, u) =
-  subst_TVars (Type.typ_match tsig (U, T) Vartab.empty) u
+fun expand_atom T (U, u) =
+  subst_TVars (Type.raw_match (U, T) Vartab.empty) u
   handle Type.TYPE_MATCH => raise TYPE ("expand_atom: ill-typed replacement", [T, U], [u]);
 
 end;