src/HOL/Tools/old_primrec_package.ML
changeset 25561 d955e1d01e6a
parent 25557 ea6b11021e79
child 26478 9d1029ce0e13
--- a/src/HOL/Tools/old_primrec_package.ML	Thu Dec 06 16:36:21 2007 +0100
+++ b/src/HOL/Tools/old_primrec_package.ML	Thu Dec 06 16:38:42 2007 +0100
@@ -17,11 +17,6 @@
     -> theory -> thm list * theory
   val add_primrec_unchecked_i: string -> ((bstring * term) * attribute list) list
     -> theory -> thm list * theory
-  (* FIXME !? *)
-  val gen_primrec: ((bstring * attribute list) * thm list -> theory -> (bstring * thm list) * theory)
-    -> ((bstring * attribute list) * term -> theory -> (bstring * thm) * theory)
-    -> string -> ((bstring * attribute list) * term) list
-    -> theory -> thm list * theory;
 end;
 
 structure OldPrimrecPackage : OLD_PRIMREC_PACKAGE =