check recursive definitions for structural descent

Add "eliminate_definition" before "eliminate_algebraic" in gappa.drv
"eliminate_recursion" or "eliminate_definition" should be always
applied before "eliminate_algebraic".

drivers/gappa.drv

@@ -13,6 +13,7 @@ transformation "simplify_recursive_definition"
 transformation "inline_trivial"
 transformation "eliminate_builtin"
 transformation "inline_all"
+transformation "eliminate_definition"
 transformation "eliminate_inductive"
 transformation "eliminate_algebraic"
 transformation "eliminate_if"

src/core/decl.ml

@@ -427,7 +427,7 @@ let create_logic_decl ldl =
         syms, news_id news ls.ls_name
   in
   let (syms,news) = List.fold_left check_decl (Sid.empty,Sid.empty) ldl in
-  (* ignore (check_termination ldl); *)
+  ignore (check_termination ldl);
   mk_decl (Dlogic ldl) syms news
 
 exception InvalidIndDecl of lsymbol * prsymbol