1.1 --- a/src/Provers/clasimp.ML	Mon Jul 05 16:46:23 2010 +0200
     1.2 +++ b/src/Provers/clasimp.ML	Mon Jul 05 16:43:08 2010 +0100
     1.3 @@ -203,7 +203,7 @@
     1.4            (CHANGED o nodup_depth_tac cs' n); (* slower but more general *)
     1.5      in  EVERY [ALLGOALS (Simplifier.asm_full_simp_tac ss),
     1.6                 TRY (Classical.safe_tac cs),
     1.7 -               REPEAT (FIRSTGOAL maintac),
     1.8 +               REPEAT_DETERM (FIRSTGOAL maintac),
     1.9                 TRY (Classical.safe_tac (cs addSss ss)),
    1.10                 prune_params_tac]
    1.11      end;

     2.1 --- a/src/Pure/unify.ML	Mon Jul 05 16:46:23 2010 +0200
     2.2 +++ b/src/Pure/unify.ML	Mon Jul 05 16:43:08 2010 +0100
     2.3 @@ -451,20 +451,23 @@
     2.4    end;
     2.5  
     2.6  
     2.7 +(*If an argument contains a banned Bound, then it should be deleted.
     2.8 +  But if the only path is flexible, this is difficult; the code gives up!
     2.9 +  In  %x y.?a(x) =?= %x y.?b(?c(y)) should we instantiate ?b or ?c *)
    2.10 +exception CHANGE_FAIL;   (*flexible occurrence of banned variable, or other reason to quit*)
    2.11 +
    2.12 +
    2.13  (*Flex argument: a term, its type, and the index that refers to it.*)
    2.14  type flarg = {t: term, T: typ, j: int};
    2.15  
    2.16  (*Form the arguments into records for deletion/sorting.*)
    2.17  fun flexargs ([], [], []) = [] : flarg list
    2.18    | flexargs (j :: js, t :: ts, T :: Ts) = {j = j, t = t, T = T} :: flexargs (js, ts, Ts)
    2.19 -  | flexargs _ = raise Fail "flexargs";
    2.20 -
    2.21 -
    2.22 -(*If an argument contains a banned Bound, then it should be deleted.
    2.23 -  But if the only path is flexible, this is difficult; the code gives up!
    2.24 -  In  %x y.?a(x) =?= %x y.?b(?c(y)) should we instantiate ?b or ?c *)
    2.25 -exception CHANGE_FAIL;   (*flexible occurrence of banned variable*)
    2.26 -
    2.27 +  | flexargs _ = raise CHANGE_FAIL;
    2.28 +(*We give up if we see a variable of function type not applied to a full list of 
    2.29 +  arguments (remember, this code assumes that terms are fully eta-expanded).  This situation 
    2.30 +  can occur if a type variable is instantiated with a function type.
    2.31 +*)
    2.32  
    2.33  (*Check whether the 'banned' bound var indices occur rigidly in t*)
    2.34  fun rigid_bound (lev, banned) t =
    2.35 @@ -516,7 +519,7 @@
    2.36      val (Var (v, T), ts) = strip_comb t;
    2.37      val (Ts, U) = strip_type env T
    2.38      and js = length ts - 1  downto 0;
    2.39 -    val args = sort (make_ord arg_less) (List.foldr (change_arg banned) [] (flexargs (js, ts, Ts)))
    2.40 +    val args = sort (make_ord arg_less) (List.foldr (change_arg banned) [] (flexargs (js, ts, Ts))) 
    2.41      val ts' = map #t args;
    2.42    in
    2.43      if decreasing (length Ts) args then (env, (list_comb (Var (v, T), ts')))