# HG changeset patch
# User berghofe
# Date 1106586430 -3600
# Node ID 9c292e3e0ca11f4b823ce8f38798395ef720121f
# Parent  1fbd4aba46e380bbe175d5d09946e84d08dd9e72
Replaced xstring by thmref.

diff -r 1fbd4aba46e3 -r 9c292e3e0ca1 src/HOL/Tools/recdef_package.ML
--- a/src/HOL/Tools/recdef_package.ML	Mon Jan 24 17:59:48 2005 +0100
+++ b/src/HOL/Tools/recdef_package.ML	Mon Jan 24 18:07:10 2005 +0100
@@ -31,7 +31,7 @@
   val add_recdef_old: xstring -> string -> ((bstring * string) * Args.src list) list ->
     simpset * thm list -> theory ->
     theory * {simps: thm list, rules: thm list list, induct: thm, tcs: term list}
-  val defer_recdef: xstring -> string list -> (xstring * Args.src list) list
+  val defer_recdef: xstring -> string list -> (thmref * Args.src list) list
     -> theory -> theory * {induct_rules: thm}
   val defer_recdef_i: xstring -> term list -> (thm list * theory attribute list) list
     -> theory -> theory * {induct_rules: thm}