src/HOL/Tools/function_package/fundef_common.ML

     FundefConfig {sequential=sequential, default=default, domintros=true,tailrec=tailrec}
   | apply_opt Tailrec (FundefConfig {sequential, default, domintros,tailrec}) =
     FundefConfig {sequential=sequential, default=default, domintros=domintros,tailrec=true}
 
 val default_config =
-  FundefConfig { sequential=false, default="%x. arbitrary", domintros=false, tailrec=false }
+  FundefConfig { sequential=false, default="%x. undefined" (*FIXME dynamic scoping*), domintros=false, tailrec=false }
 
 
 (* Analyzing function equations *)
 
 fun split_def ctxt geq =