# HG changeset patch
# User haftmann
# Date 1196955522 -3600
# Node ID d955e1d01e6a4a044fcfab12162773dbbb3a506f
# Parent  63be39eeb41a8873711db07e8c113c69174eb463
-authentic primrec

diff -r 63be39eeb41a -r d955e1d01e6a src/HOL/Tools/old_primrec_package.ML
--- 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 =