+let goal_symbols = ref TermSet.empty
+
+let set_of_map m =
+ TermMap.fold (fun k _ s -> TermSet.add k s) m TermSet.empty
+;;
+
+let set_goal_symbols term =
+ let m = symbols_of_term term in
+ goal_symbols := (set_of_map m)
+;;
+
+let symbols_of_eq (ty,left,right,_) =
+ let sty = set_of_map (symbols_of_term ty) in
+ let sl = set_of_map (symbols_of_term left) in
+ let sr = set_of_map (symbols_of_term right) in
+ TermSet.union sty (TermSet.union sl sr)
+;;
+
+let distance sgoal seq =
+ let s = TermSet.diff seq sgoal in
+ TermSet.cardinal s
+;;
+