# HG changeset patch
# User wenzelm
# Date 1247864051 -7200
# Node ID 70c0bcd0adfbd80560fb80d1232083b5ded8caad
# Parent  f92df23c33057765b8bac9035f2354350c74a436
tuned/modernized subst: Same.operation;
renamed typ_subst_TVars to subst_type;
renamed subst_TVars to subst_term_types;
renamed subst_vars to subst_term;
removed unused subst_Vars (covered by subst_term);

diff -r f92df23c3305 -r 70c0bcd0adfb src/Pure/envir.ML
--- a/src/Pure/envir.ML	Fri Jul 17 22:51:18 2009 +0200
+++ b/src/Pure/envir.ML	Fri Jul 17 22:54:11 2009 +0200
@@ -34,10 +34,12 @@
   val eta_contract: term -> term
   val beta_eta_contract: term -> term
   val fastype: env -> typ list -> term -> typ
-  val typ_subst_TVars: Type.tyenv -> typ -> typ
-  val subst_TVars: Type.tyenv -> term -> term
-  val subst_Vars: tenv -> term -> term
-  val subst_vars: Type.tyenv * tenv -> term -> term
+  val subst_type_same: Type.tyenv -> typ Same.operation
+  val subst_term_types_same: Type.tyenv -> term Same.operation
+  val subst_term_same: Type.tyenv * tenv -> term Same.operation
+  val subst_type: Type.tyenv -> typ -> typ
+  val subst_term_types: Type.tyenv -> term -> term
+  val subst_term: Type.tyenv * tenv -> term -> term
   val expand_atom: typ -> typ * term -> term
   val expand_term: (term -> (typ * term) option) -> term -> term
   val expand_term_frees: ((string * typ) * term) list -> term -> term
@@ -296,51 +298,68 @@
   in fast end;
 
 
-(*Substitute for type Vars in a type*)
-fun typ_subst_TVars tyenv T =
-  if Vartab.is_empty tyenv then T
-  else
-    let
-      fun subst (Type (a, Ts)) = Type (a, map subst Ts)
-        | subst (T as TFree _) = T
-        | subst (T as TVar v) = (case Type.lookup tyenv v of NONE => T | SOME U => U);
-    in subst T end;
+
+(** plain substitution -- without variable chasing **)
+
+local
 
-(*Substitute for type Vars in a term*)
-val subst_TVars = map_types o typ_subst_TVars;
+fun subst_type0 tyenv = Term_Subst.map_atypsT_same
+  (fn TVar v =>
+        (case Type.lookup tyenv v of
+          SOME U => U
+        | NONE => raise Same.SAME)
+    | _ => raise Same.SAME);
+
+fun subst_term1 tenv = Term_Subst.map_aterms_same
+  (fn Var v =>
+        (case lookup' (tenv, v) of
+          SOME u => u
+        | NONE => raise Same.SAME)
+    | _ => raise Same.SAME);
 
-(*Substitute for Vars in a term *)
-fun subst_Vars tenv tm =
-  if Vartab.is_empty tenv then tm
-  else
-    let
-      fun subst (t as Var v) = the_default t (lookup' (tenv, v))
-        | subst (Abs (a, T, t)) = Abs (a, T, subst t)
-        | subst (t $ u) = subst t $ subst u
-        | subst t = t;
-    in subst tm end;
+fun subst_term2 tenv tyenv : term Same.operation =
+  let
+    val substT = subst_type0 tyenv;
+    fun subst (Const (a, T)) = Const (a, substT T)
+      | subst (Free (a, T)) = Free (a, substT T)
+      | subst (Var (xi, T)) =
+          (case lookup' (tenv, (xi, T)) of
+            SOME u => u
+          | NONE => Var (xi, substT T))
+      | subst (Bound _) = raise Same.SAME
+      | subst (Abs (a, T, t)) =
+          (Abs (a, substT T, Same.commit subst t)
+            handle Same.SAME => Abs (a, T, subst t))
+      | subst (t $ u) = (subst t $ Same.commit subst u handle Same.SAME => t $ subst u);
+  in subst end;
+
+in
 
-(*Substitute for type/term Vars in a term *)
-fun subst_vars (tyenv, tenv) =
-  if Vartab.is_empty tyenv then subst_Vars tenv
-  else
-    let
-      fun subst (Const (a, T)) = Const (a, typ_subst_TVars tyenv T)
-        | subst (Free (a, T)) = Free (a, typ_subst_TVars tyenv T)
-        | subst (Var (xi, T)) =
-            (case lookup' (tenv, (xi, T)) of
-              NONE => Var (xi, typ_subst_TVars tyenv T)
-            | SOME t => t)
-        | subst (t as Bound _) = t
-        | subst (Abs (a, T, t)) = Abs (a, typ_subst_TVars tyenv T, subst t)
-        | subst (t $ u) = subst t $ subst u;
-    in subst end;
+fun subst_type_same tyenv T =
+  if Vartab.is_empty tyenv then raise Same.SAME
+  else subst_type0 tyenv T;
+
+fun subst_term_types_same tyenv t =
+  if Vartab.is_empty tyenv then raise Same.SAME
+  else Term_Subst.map_types_same (subst_type0 tyenv) t;
+
+fun subst_term_same (tyenv, tenv) =
+  if Vartab.is_empty tenv then subst_term_types_same tyenv
+  else if Vartab.is_empty tyenv then subst_term1 tenv
+  else subst_term2 tenv tyenv;
+
+fun subst_type tyenv T = subst_type_same tyenv T handle Same.SAME => T;
+fun subst_term_types tyenv t = subst_term_types_same tyenv t handle Same.SAME => t;
+fun subst_term envs t = subst_term_same envs t handle Same.SAME => t;
+
+end;
 
 
-(* expand defined atoms -- with local beta reduction *)
+
+(** expand defined atoms -- with local beta reduction **)
 
 fun expand_atom T (U, u) =
-  subst_TVars (Type.raw_match (U, T) Vartab.empty) u
+  subst_term_types (Type.raw_match (U, T) Vartab.empty) u
     handle Type.TYPE_MATCH => raise TYPE ("expand_atom: ill-typed replacement", [T, U], [u]);
 
 fun expand_term get =