src/HOL/Tools/Function/function_common.ML

 
 datatype function_result = FunctionResult of
  {fs: term list,
   G: term,
   R: term,
-
   psimps : thm list,
-  trsimps : thm list option,
-
   simple_pinducts : thm list,
   cases : thm,
   termination : thm,
   domintros : thm list option}
 

 datatype function_opt
   = Sequential
   | Default of string
   | DomIntros
   | No_Partials
-  | Tailrec
 
 datatype function_config = FunctionConfig of
  {sequential: bool,
   default: string option,
   domintros: bool,
-  partials: bool,
-  tailrec: bool}
-
-fun apply_opt Sequential (FunctionConfig {sequential, default, domintros, partials, tailrec}) =
-    FunctionConfig {sequential=true, default=default, domintros=domintros, partials=partials, tailrec=tailrec}
-  | apply_opt (Default d) (FunctionConfig {sequential, default, domintros, partials, tailrec}) =
-    FunctionConfig {sequential=sequential, default=SOME d, domintros=domintros, partials=partials, tailrec=tailrec}
-  | apply_opt DomIntros (FunctionConfig {sequential, default, domintros, partials, tailrec}) =
-    FunctionConfig {sequential=sequential, default=default, domintros=true, partials=partials, tailrec=tailrec}
-  | apply_opt Tailrec (FunctionConfig {sequential, default, domintros, partials, tailrec}) =
-    FunctionConfig {sequential=sequential, default=default, domintros=domintros, partials=partials, tailrec=true}
-  | apply_opt No_Partials (FunctionConfig {sequential, default, domintros, partials, tailrec}) =
-    FunctionConfig {sequential=sequential, default=default, domintros=domintros, partials=false, tailrec=true}
+  partials: bool}
+
+fun apply_opt Sequential (FunctionConfig {sequential, default, domintros, partials}) =
+    FunctionConfig {sequential=true, default=default, domintros=domintros, partials=partials}
+  | apply_opt (Default d) (FunctionConfig {sequential, default, domintros, partials}) =
+    FunctionConfig {sequential=sequential, default=SOME d, domintros=domintros, partials=partials}
+  | apply_opt DomIntros (FunctionConfig {sequential, default, domintros, partials}) =
+    FunctionConfig {sequential=sequential, default=default, domintros=true, partials=partials}
+  | apply_opt No_Partials (FunctionConfig {sequential, default, domintros, partials}) =
+    FunctionConfig {sequential=sequential, default=default, domintros=domintros, partials=false}
 
 val default_config =
   FunctionConfig { sequential=false, default=NONE,
-    domintros=false, partials=true, tailrec=false }
+    domintros=false, partials=true}
 
 
 (* Analyzing function equations *)
 
 fun split_def ctxt check_head geq =

 local
   val option_parser = Parse.group "option"
     ((Parse.reserved "sequential" >> K Sequential)
      || ((Parse.reserved "default" |-- Parse.term) >> Default)
      || (Parse.reserved "domintros" >> K DomIntros)
-     || (Parse.reserved "no_partials" >> K No_Partials)
-     || (Parse.reserved "tailrec" >> K Tailrec))
+     || (Parse.reserved "no_partials" >> K No_Partials))
 
   fun config_parser default =
     (Scan.optional (Parse.$$$ "(" |-- Parse.!!! (Parse.list1 option_parser) --| Parse.$$$ ")") [])
      >> (fn opts => fold apply_opt opts default)
 in