1.1 --- a/src/Pure/unify.ML	Thu Dec 30 22:07:18 2010 +0100
     1.2 +++ b/src/Pure/unify.ML	Thu Dec 30 22:34:53 2010 +0100
     1.3 @@ -205,14 +205,6 @@
     1.4  exception ASSIGN;  (*Raised if not an assignment*)
     1.5  
     1.6  
     1.7 -fun self_asgt (ix,(_,TVar (ix',_))) = (ix = ix')
     1.8 -  | self_asgt (ix, _) = false;
     1.9 -
    1.10 -fun check_tyenv msg tys tyenv = 
    1.11 -  if Vartab.exists self_asgt tyenv
    1.12 -  then raise TYPE (msg ^ ": looping type envir!!", tys, []) 
    1.13 -  else tyenv;
    1.14 -
    1.15  fun unify_types thy (T, U, env) =
    1.16    if T = U then env
    1.17    else
    1.18 @@ -472,8 +464,8 @@
    1.19  fun flexargs ([], [], []) = [] : flarg list
    1.20    | flexargs (j :: js, t :: ts, T :: Ts) = {j = j, t = t, T = T} :: flexargs (js, ts, Ts)
    1.21    | flexargs _ = raise CHANGE_FAIL;
    1.22 -(*We give up if we see a variable of function type not applied to a full list of 
    1.23 -  arguments (remember, this code assumes that terms are fully eta-expanded).  This situation 
    1.24 +(*We give up if we see a variable of function type not applied to a full list of
    1.25 +  arguments (remember, this code assumes that terms are fully eta-expanded).  This situation
    1.26    can occur if a type variable is instantiated with a function type.
    1.27  *)
    1.28  
    1.29 @@ -527,7 +519,7 @@
    1.30      val (Var (v, T), ts) = strip_comb t;
    1.31      val (Ts, U) = strip_type env T
    1.32      and js = length ts - 1  downto 0;
    1.33 -    val args = sort (make_ord arg_less) (List.foldr (change_arg banned) [] (flexargs (js, ts, Ts))) 
    1.34 +    val args = sort (make_ord arg_less) (List.foldr (change_arg banned) [] (flexargs (js, ts, Ts)))
    1.35      val ts' = map #t args;
    1.36    in
    1.37      if decreasing (length Ts) args then (env, (list_comb (Var (v, T), ts')))
    1.38 @@ -690,7 +682,7 @@
    1.39    in Seq.single (Envir.Envir {maxidx = maxidx, tenv = tenv', tyenv = tyenv'}) end
    1.40    handle Pattern.MATCH => Seq.empty;
    1.41  
    1.42 -(*General matching -- keeps variables disjoint*)
    1.43 +(*General matching -- keep variables disjoint*)
    1.44  fun matchers _ [] = Seq.single (Envir.empty ~1)
    1.45    | matchers thy pairs =
    1.46        let
    1.47 @@ -711,20 +703,29 @@
    1.48              if i > maxidx then Var ((x, i - offset), T) else t | t => t);
    1.49  
    1.50          fun norm_tvar env ((x, i), S) =
    1.51 -          ((x, i - offset),
    1.52 -            (S, decr_indexesT (Envir.norm_type (Envir.type_env env) (TVar ((x, i), S)))));
    1.53 +          let
    1.54 +            val tyenv = Envir.type_env env;
    1.55 +            val T' = Envir.norm_type tyenv (TVar ((x, i), S));
    1.56 +          in
    1.57 +            if (case T' of TVar (v, _) => v = (x, i) | _ => false) then NONE
    1.58 +            else SOME ((x, i - offset), (S, decr_indexesT T'))
    1.59 +          end;
    1.60 +
    1.61          fun norm_var env ((x, i), T) =
    1.62            let
    1.63              val tyenv = Envir.type_env env;
    1.64              val T' = Envir.norm_type tyenv T;
    1.65              val t' = Envir.norm_term env (Var ((x, i), T'));
    1.66 -          in ((x, i - offset), (decr_indexesT T', decr_indexes t')) end;
    1.67 +          in
    1.68 +            if (case t' of Var (v, _) => v = (x, i) | _ => false) then NONE
    1.69 +            else SOME ((x, i - offset), (decr_indexesT T', decr_indexes t'))
    1.70 +          end;
    1.71  
    1.72          fun result env =
    1.73            if Envir.above env maxidx then   (* FIXME proper handling of generated vars!? *)
    1.74              SOME (Envir.Envir {maxidx = maxidx,
    1.75 -              tyenv = Vartab.make (filter_out self_asgt (map (norm_tvar env) pat_tvars)),
    1.76 -              tenv = Vartab.make (map (norm_var env) pat_vars)})
    1.77 +              tyenv = Vartab.make (map_filter (norm_tvar env) pat_tvars),
    1.78 +              tenv = Vartab.make (map_filter (norm_var env) pat_vars)})
    1.79            else NONE;
    1.80  
    1.81          val empty = Envir.empty maxidx';