X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=ocaml%2Flambda4.ml;h=570691e1be16101622515e0d8c55a70bceda31bc;hb=eb8bb784b35d303a1c239f30008cba79f658f4b3;hp=35f03ca8bf4af09dc6bde54560cc789edbff12e7;hpb=1bef432e151246cbcd9776da9cef4f0c038d387e;p=fireball-separation.git

diff --git a/ocaml/lambda4.ml b/ocaml/lambda4.ml
index 35f03ca..570691e 100644
--- a/ocaml/lambda4.ml
+++ b/ocaml/lambda4.ml
@@ -499,8 +499,12 @@ let auto_instantiate (n,p) =
        fun t -> match t with `Var _ -> None | x -> if arity_of_hd x <= 0 then None else hd_of x
       ) ((match p.div with Some t -> [(t :> i_n_var)] | _ -> []) @ p.ps)) in
      (match heads with
-         [] ->
-         assert false
+         [] -> (
+          try
+           fst (List.find (((<) 0) ++ snd) (concat_map free_vars' (p.conv :> nf list)))
+          with
+           Not_found -> assert false
+          )
        | x::_ ->
           prerr_endline ("INSTANTIATING TO EAT " ^ string_of_var x);
           x)