# HG changeset patch
# User wenzelm
# Date 1277841391 -7200
# Node ID ab50854da8970c9fba0619622503cce74fbbf028
# Parent  484efa6509079a995c70f83f06ed4361a1baa467
eliminated some unused bindings;

diff -r 484efa650907 -r ab50854da897 src/Pure/unify.ML
--- a/src/Pure/unify.ML	Tue Jun 29 21:46:47 2010 +0200
+++ b/src/Pure/unify.ML	Tue Jun 29 21:56:31 2010 +0200
@@ -67,7 +67,7 @@
   let
     val tyenv = Envir.type_env env;
     fun bTs (Type ("fun", [T, U])) = T :: bTs U
-      | bTs (T as TVar v) =
+      | bTs (TVar v) =
           (case Type.lookup tyenv v of
             NONE => []
           | SOME T' => bTs T')
@@ -110,7 +110,7 @@
       env: Envir.env, v: indexname, ts: term list): bool =
   let
     fun occurs [] = false
-      | occurs (t::ts) =  occur t  orelse  occurs ts
+      | occurs (t :: ts) = occur t orelse occurs ts
     and occur (Const _) = false
       | occur (Bound _) = false
       | occur (Free _) = false
@@ -196,7 +196,7 @@
             Var (w,_) => (*w is not assigned*)
               if Term.eq_ix (v, w) then Rigid
               else nonrigid t
-          | Abs (_, _, body) => nonrigid t (*not in normal form*)
+          | Abs _ => nonrigid t (*not in normal form*)
           | _ => occomb t)
   in occur t end;
 
@@ -331,7 +331,7 @@
   The B.j are bound vars of binder.
   The terms are not made in eta-normal-form, SIMPL does that later.
   If done here, eta-expansion must be recursive in the arguments! *)
-fun make_args name (binder: typ list, env, []) = (env, [])   (*frequent case*)
+fun make_args _ (_, env, []) = (env, [])   (*frequent case*)
   | make_args name (binder: typ list, env, Ts) : Envir.env * term list =
       let
         fun funtype T = binder ---> T;
@@ -410,7 +410,7 @@
         Abs (a, T, body) =>
           Seq.map (fn (body', ed') => (Abs (a, T, body'), ed'))
             (mc ((a, T) :: rbinder, (map (incr_boundvars 1) targs) @ [Bound 0], body, ed))
-      | Var (w, uary) =>
+      | Var (w, _) =>
           (*a flex-flex dpair: make variable for t*)
           let
             val (env', newhd) = Envir.genvar (#1 w) (env, Ts ---> base);
@@ -652,7 +652,7 @@
   Unlike Huet (1975), does not smash together all variables of same type --
     requires more work yet gives a less general unifier (fewer variables).
   Handles ?f(t1...rm) with ?f(u1...um) to avoid multiple updates. *)
-fun smash_flexflex1 ((t,u), env) : Envir.env =
+fun smash_flexflex1 ((t, u), env) : Envir.env =
   let
     val vT as (v, T) = var_head_of (env, t)
     and wU as (w, U) = var_head_of (env, u);
@@ -665,7 +665,7 @@
 
 
 (*Smash all flex-flexpairs.  Should allow selection of pairs by a predicate?*)
-fun smash_flexflex (env,tpairs) : Envir.env =
+fun smash_flexflex (env, tpairs) : Envir.env =
   List.foldr smash_flexflex1 env tpairs;
 
 (*Returns unifiers with no remaining disagreement pairs*)