get_recdef now returns None instead of raising ERROR.
authorberghofe
Wed Mar 15 23:40:59 2000 +0100 (2000-03-15)
changeset 848189d498a8d3f6
parent 8480 50266d517b0c
child 8482 bbc805ebc904
get_recdef now returns None instead of raising ERROR.
src/HOL/Tools/recdef_package.ML
     1.1 --- a/src/HOL/Tools/recdef_package.ML	Wed Mar 15 23:39:45 2000 +0100
     1.2 +++ b/src/HOL/Tools/recdef_package.ML	Wed Mar 15 23:40:59 2000 +0100
     1.3 @@ -9,7 +9,7 @@
     1.4  sig
     1.5    val quiet_mode: bool ref
     1.6    val print_recdefs: theory -> unit
     1.7 -  val get_recdef: theory -> string -> {rules: thm list, induct: thm, tcs: term list}
     1.8 +  val get_recdef: theory -> string -> {rules: thm list, induct: thm, tcs: term list} option
     1.9    val add_recdef: xstring -> string -> string list -> simpset option
    1.10      -> (xstring * Args.src list) list -> theory
    1.11      -> theory * {rules: thm list, induct: thm, tcs: term list}
    1.12 @@ -58,10 +58,7 @@
    1.13  
    1.14  (* get and put data *)
    1.15  
    1.16 -fun get_recdef thy name =
    1.17 -  (case Symtab.lookup (RecdefData.get thy, name) of
    1.18 -    Some info => info
    1.19 -  | None => error ("Unknown recursive function " ^ quote name));
    1.20 +fun get_recdef thy name = Symtab.lookup (RecdefData.get thy, name);
    1.21  
    1.22  fun put_recdef name info thy =
    1.23    let