src/Pure/thm.ML
changeset 4847 ea7d7a65e4e9
parent 4820 8f6dbbd8d497
child 4999 4c74267cfa0c
     1.1 --- a/src/Pure/thm.ML	Wed Apr 29 11:17:14 1998 +0200
     1.2 +++ b/src/Pure/thm.ML	Wed Apr 29 11:20:53 1998 +0200
     1.3 @@ -103,6 +103,7 @@
     1.4    val strip_shyps       : thm -> thm
     1.5    val implies_intr_shyps: thm -> thm
     1.6    val get_axiom         : theory -> xstring -> thm
     1.7 +  val get_def           : theory -> xstring -> thm
     1.8    val name_thm          : string * thm -> thm
     1.9    val name_of_thm	: thm -> string
    1.10    val axioms_of         : theory -> (string * thm) list
    1.11 @@ -574,25 +575,30 @@
    1.12  (*look up the named axiom in the theory*)
    1.13  fun get_axiom theory raw_name =
    1.14    let
    1.15 -    val name = Sign.intern (sign_of theory) Theory.axiomK raw_name;
    1.16 -    fun get_ax [] = raise Match
    1.17 +    val name = Sign.intern (Theory.sign_of theory) Theory.axiomK raw_name;
    1.18 +
    1.19 +    fun get_ax [] = None
    1.20        | get_ax (thy :: thys) =
    1.21 -          let val {sign, axioms, parents, ...} = rep_theory thy
    1.22 -          in case Symtab.lookup (axioms, name) of
    1.23 -                Some t => fix_shyps [] []
    1.24 -                           (Thm {sign_ref = Sign.self_ref sign,
    1.25 -                                 der = infer_derivs (Axiom name, []),
    1.26 -                                 maxidx = maxidx_of_term t,
    1.27 -                                 shyps = [], 
    1.28 -                                 hyps = [], 
    1.29 -                                 prop = t})
    1.30 -              | None => get_ax parents handle Match => get_ax thys
    1.31 +          let val {sign, axioms, ...} = Theory.rep_theory thy in
    1.32 +            (case Symtab.lookup (axioms, name) of
    1.33 +              Some t =>
    1.34 +                Some (fix_shyps [] []
    1.35 +                  (Thm {sign_ref = Sign.self_ref sign,
    1.36 +                    der = infer_derivs (Axiom name, []),
    1.37 +                    maxidx = maxidx_of_term t,
    1.38 +                    shyps = [], 
    1.39 +                    hyps = [], 
    1.40 +                    prop = t}))
    1.41 +            | None => get_ax thys)
    1.42            end;
    1.43    in
    1.44 -    get_ax [theory] handle Match
    1.45 -      => raise THEORY ("No axiom " ^ quote name, [theory])
    1.46 +    (case get_ax (theory :: Theory.ancestors_of theory) of
    1.47 +      Some thm => thm
    1.48 +    | None => raise THEORY ("No axiom " ^ quote name, [theory]))
    1.49    end;
    1.50  
    1.51 +fun get_def thy name = get_axiom thy (name ^ "_def");
    1.52 +
    1.53  
    1.54  (*return additional axioms of this theory node*)
    1.55  fun axioms_of thy =