Embarassing bug in eta_eq fixed

diff --git a/ocaml/simple.ml b/ocaml/simple.ml
index c7b9a3a9998e33b5eeb822c416196373a536ceed..b1b05eca5c43f8f81429836ccda109d10f5c317b 100644 (file)
--- a/ocaml/simple.ml
+++ b/ocaml/simple.ml
@@ -21,19 +21,6 @@ type t =
  | L of t\r
 ;;\r
 \r
-let measure_of_t =\r
- let rec aux acc = function\r
- | V _ -> acc, 0\r
- | A(b,t1,t2) ->\r
-   let acc, m1 = aux acc t1 in\r
-   let acc, m2 = aux acc t2 in\r
-   (match b with\r
-   | `Some b when !b && not (List.memq b acc) -> b::acc, 1 + m1 + m2\r
-   | _ -> acc, m1 + m2)\r
- | L t -> aux acc t\r
- in snd ++ (aux [])\r
-;;\r
-\r
 let index_of x =\r
  let rec aux n =\r
   function\r
@@ -88,6 +75,19 @@ let delta = L(A(`Some (ref true),V 0, V 0));;
 (* does NOT lift the argument *)\r
 let mk_lams = fold_nat (fun x _ -> L x) ;;\r
 \r
+let measure_of_t =\r
+ let rec aux acc = function\r
+ | V _ -> acc, 0\r
+ | A(b,t1,t2) ->\r
+   let acc, m1 = aux acc t1 in\r
+   let acc, m2 = aux acc t2 in\r
+   (match b with\r
+   | `Some b when !b && not (List.memq b acc) -> b::acc, 1 + m1 + m2\r
+   | _ -> acc, m1 + m2)\r
+ | L t -> aux acc t\r
+ in snd ++ (aux [])\r
+;;\r
+\r
 type problem = {\r
    orig_freshno: int\r
  ; freshno : int\r