get_inductive now returns None instead of raising an exception.
authorberghofe
Fri Jun 23 12:29:55 2000 +0200 (2000-06-23)
changeset 91169df44b5c610b
parent 9115 67409447f788
child 9117 48ccddd9fdfe
get_inductive now returns None instead of raising an exception.
src/HOL/Tools/inductive_package.ML
     1.1 --- a/src/HOL/Tools/inductive_package.ML	Fri Jun 23 12:28:09 2000 +0200
     1.2 +++ b/src/HOL/Tools/inductive_package.ML	Fri Jun 23 12:29:55 2000 +0200
     1.3 @@ -32,9 +32,9 @@
     1.4  sig
     1.5    val quiet_mode: bool ref
     1.6    val unify_consts: Sign.sg -> term list -> term list -> term list * term list
     1.7 -  val get_inductive: theory -> string ->
     1.8 -    {names: string list, coind: bool} * {defs: thm list, elims: thm list, raw_induct: thm,
     1.9 -      induct: thm, intrs: thm list, mk_cases: string -> thm, mono: thm, unfold: thm}
    1.10 +  val get_inductive: theory -> string -> ({names: string list, coind: bool} *
    1.11 +    {defs: thm list, elims: thm list, raw_induct: thm, induct: thm,
    1.12 +     intrs: thm list, mk_cases: string -> thm, mono: thm, unfold: thm}) option
    1.13    val print_inductives: theory -> unit
    1.14    val mono_add_global: theory attribute
    1.15    val mono_del_global: theory attribute
    1.16 @@ -90,10 +90,7 @@
    1.17  
    1.18  (* get and put data *)
    1.19  
    1.20 -fun get_inductive thy name =
    1.21 -  (case Symtab.lookup (fst (InductiveData.get thy), name) of
    1.22 -    Some info => info
    1.23 -  | None => error ("Unknown (co)inductive set " ^ quote name));
    1.24 +fun get_inductive thy name = Symtab.lookup (fst (InductiveData.get thy), name);
    1.25  
    1.26  fun put_inductives names info thy =
    1.27    let
    1.28 @@ -497,16 +494,20 @@
    1.29  
    1.30  fun gen_inductive_cases prep_att prep_const prep_prop
    1.31      ((((name, raw_atts), raw_set), raw_props), comment) thy =
    1.32 -  let
    1.33 -    val sign = Theory.sign_of thy;
    1.34 -
    1.35 -    val atts = map (prep_att thy) raw_atts;
    1.36 -    val (_, {elims, ...}) = get_inductive thy (prep_const sign raw_set);
    1.37 -    val cprops = map (Thm.cterm_of sign o prep_prop (ProofContext.init thy)) raw_props;
    1.38 -    val thms = map (mk_cases_i true elims (Simplifier.simpset_of thy)) cprops;
    1.39 -  in
    1.40 -    thy
    1.41 -    |> IsarThy.have_theorems_i (((name, atts), map Thm.no_attributes thms), comment)
    1.42 +  let val sign = Theory.sign_of thy;
    1.43 +  in (case get_inductive thy (prep_const sign raw_set) of
    1.44 +      None => error ("Unknown (co)inductive set " ^ quote name)
    1.45 +    | Some (_, {elims, ...}) =>
    1.46 +        let
    1.47 +          val atts = map (prep_att thy) raw_atts;
    1.48 +          val cprops = map
    1.49 +            (Thm.cterm_of sign o prep_prop (ProofContext.init thy)) raw_props;
    1.50 +          val thms = map
    1.51 +            (mk_cases_i true elims (Simplifier.simpset_of thy)) cprops;
    1.52 +        in
    1.53 +          thy |> IsarThy.have_theorems_i
    1.54 +            (((name, atts), map Thm.no_attributes thms), comment)
    1.55 +        end)
    1.56    end;
    1.57  
    1.58  val inductive_cases =