# HG changeset patch
# User berghofe
# Date 953160059 -3600
# Node ID 89d498a8d3f602d646ff741bf7d4655a22cff3e5
# Parent  50266d517b0c02cb92f97c746a7a2d434b2ac044
get_recdef now returns None instead of raising ERROR.

diff -r 50266d517b0c -r 89d498a8d3f6 src/HOL/Tools/recdef_package.ML
--- a/src/HOL/Tools/recdef_package.ML	Wed Mar 15 23:39:45 2000 +0100
+++ b/src/HOL/Tools/recdef_package.ML	Wed Mar 15 23:40:59 2000 +0100
@@ -9,7 +9,7 @@
 sig
   val quiet_mode: bool ref
   val print_recdefs: theory -> unit
-  val get_recdef: theory -> string -> {rules: thm list, induct: thm, tcs: term list}
+  val get_recdef: theory -> string -> {rules: thm list, induct: thm, tcs: term list} option
   val add_recdef: xstring -> string -> string list -> simpset option
     -> (xstring * Args.src list) list -> theory
     -> theory * {rules: thm list, induct: thm, tcs: term list}
@@ -58,10 +58,7 @@
 
 (* get and put data *)
 
-fun get_recdef thy name =
-  (case Symtab.lookup (RecdefData.get thy, name) of
-    Some info => info
-  | None => error ("Unknown recursive function " ^ quote name));
+fun get_recdef thy name = Symtab.lookup (RecdefData.get thy, name);
 
 fun put_recdef name info thy =
   let