Fix search to resolve abbreviations by expanding their body

Previously, searching for a bare abbreviation name (e.g. `search mu1`)
would wrap the abbreviation body in a lambda over its arguments, producing
a pattern like `fun d x => mu d (pred1 x)`. No axiom contains such a
lambda as a subformula, so the search always returned no results.

Instead, register the abbreviation arguments as pattern variables and use
the body directly as the search pattern. This correctly matches axioms
containing the expanded form of the abbreviation.

Author: strub

src/ecScope.ml

@@ -2684,11 +2684,11 @@ end
                     let es = e_subst tip in
                     let xs  = List.map (snd_map (ty_subst tip)) nt.ont_args in
                     let bd  = EcFol.form_of_expr (es nt.ont_body) in
-                    let fp  = EcFol.f_lambda (List.map (snd_map EcFol.gtty) xs) bd in
+                    List.iter (fun (id, ty) -> ps := Mid.add id ty !ps) xs;
 
-                    match fp.f_node with
+                    match bd.f_node with
                     | Fop (pf, _) -> (pf :: paths, pts)
-                    | _ -> (paths, (ps, ue, fp) ::pts)
+                    | _ -> (paths, (ps, ue, bd) ::pts)
                   end
 
                   | _ -> (p :: paths, pts) in