# HG changeset patch
# User wenzelm
# Date 924093773 -7200
# Node ID 9540aa1b5a9a4a31a7caa5a805972b3f68f9ed52
# Parent  ceab9e663e080b471c7bf20ebd2a2abf80863b0c
tuned comments;
tuned types;

diff -r ceab9e663e08 -r 9540aa1b5a9a src/HOL/Tools/primrec_package.ML
--- a/src/HOL/Tools/primrec_package.ML	Wed Apr 14 14:42:23 1999 +0200
+++ b/src/HOL/Tools/primrec_package.ML	Wed Apr 14 14:42:53 1999 +0200
@@ -4,17 +4,13 @@
     Copyright   1998  TU Muenchen
 
 Package for defining functions on datatypes by primitive recursion.
-
-TODO:
-  - add_primrec(_i): improve prep of args;
-  - quiet_mode (!?);
 *)
 
 signature PRIMREC_PACKAGE =
 sig
-  val add_primrec: string -> ((string * string) * Args.src list) list
+  val add_primrec: string -> ((bstring * string) * Args.src list) list
     -> theory -> theory * thm list
-  val add_primrec_i: string -> ((string * term) * theory attribute list) list
+  val add_primrec_i: string -> ((bstring * term) * theory attribute list) list
     -> theory -> theory * thm list
 end;