merged

--- a/src/Provers/clasimp.ML	Mon Jul 05 14:35:00 2010 +0200
+++ b/src/Provers/clasimp.ML	Mon Jul 05 14:21:53 2010 +0100
@@ -203,7 +203,7 @@
           (CHANGED o nodup_depth_tac cs' n); (* slower but more general *)
     in  EVERY [ALLGOALS (Simplifier.asm_full_simp_tac ss),
                TRY (Classical.safe_tac cs),
-               REPEAT (FIRSTGOAL maintac),
+               REPEAT_DETERM (FIRSTGOAL maintac),
                TRY (Classical.safe_tac (cs addSss ss)),
                prune_params_tac]
     end;

--- a/src/Pure/unify.ML	Mon Jul 05 14:35:00 2010 +0200
+++ b/src/Pure/unify.ML	Mon Jul 05 14:21:53 2010 +0100
@@ -451,20 +451,23 @@
   end;
 
 
+(*If an argument contains a banned Bound, then it should be deleted.
+  But if the only path is flexible, this is difficult; the code gives up!
+  In  %x y.?a(x) =?= %x y.?b(?c(y)) should we instantiate ?b or ?c *)
+exception CHANGE_FAIL;   (*flexible occurrence of banned variable, or other reason to quit*)
+
+
 (*Flex argument: a term, its type, and the index that refers to it.*)
 type flarg = {t: term, T: typ, j: int};
 
 (*Form the arguments into records for deletion/sorting.*)
 fun flexargs ([], [], []) = [] : flarg list
   | flexargs (j :: js, t :: ts, T :: Ts) = {j = j, t = t, T = T} :: flexargs (js, ts, Ts)
-  | flexargs _ = raise Fail "flexargs";
-
-
-(*If an argument contains a banned Bound, then it should be deleted.
-  But if the only path is flexible, this is difficult; the code gives up!
-  In  %x y.?a(x) =?= %x y.?b(?c(y)) should we instantiate ?b or ?c *)
-exception CHANGE_FAIL;   (*flexible occurrence of banned variable*)
-
+  | flexargs _ = raise CHANGE_FAIL;
+(*We give up if we see a variable of function type not applied to a full list of 
+  arguments (remember, this code assumes that terms are fully eta-expanded).  This situation 
+  can occur if a type variable is instantiated with a function type.
+*)
 
 (*Check whether the 'banned' bound var indices occur rigidly in t*)
 fun rigid_bound (lev, banned) t =
@@ -516,7 +519,7 @@
     val (Var (v, T), ts) = strip_comb t;
     val (Ts, U) = strip_type env T
     and js = length ts - 1  downto 0;
-    val args = sort (make_ord arg_less) (List.foldr (change_arg banned) [] (flexargs (js, ts, Ts)))
+    val args = sort (make_ord arg_less) (List.foldr (change_arg banned) [] (flexargs (js, ts, Ts))) 
     val ts' = map #t args;
   in
     if decreasing (length Ts) args then (env, (list_comb (Var (v, T), ts')))