Lines Matching defs:fy
29 of (fy,y::ys) =>
31 val (fy',ys,fx',xs) = if 0 < diff then (list_mk_comb(fy,(List.take(y::ys,diff))),List.drop(y::ys,diff),fx,x::xs)
32 else (fy,y::ys,list_mk_comb(fx,(List.take(x::xs,~diff))),List.drop(x::xs,~diff))
35 (if is_var fx' then (subst [inst_it fx' fy' fx' |-> fy'])
36 else (if same_const fx' fy' then I
37 else (if is_var fy' then (subst [inst_it fy' fx' fy' |-> fx'] o inst_it fy' fx') else raise match)))
39 | (fy,[]) => if is_var fy then subst [inst_it fy t1 fy |-> t1] o inst_it fy t1 else raise match)