src/Pure/thm.ML
changeset 30342 d32daa6aba3c
parent 30288 a32700e45ab3
child 30466 5f31e24937c5
     1.1 --- a/src/Pure/thm.ML	Sat Mar 07 21:57:36 2009 +0100
     1.2 +++ b/src/Pure/thm.ML	Sat Mar 07 22:04:59 2009 +0100
     1.3 @@ -128,9 +128,6 @@
     1.4    val hyps_of: thm -> term list
     1.5    val full_prop_of: thm -> term
     1.6    val axiom: theory -> string -> thm
     1.7 -  val def_name: string -> string
     1.8 -  val def_name_optional: string -> string -> string
     1.9 -  val get_def: theory -> xstring -> thm
    1.10    val axioms_of: theory -> (string * thm) list
    1.11    val get_name: thm -> string
    1.12    val put_name: string -> thm -> thm
    1.13 @@ -558,14 +555,6 @@
    1.14      | NONE => raise THEORY ("No axiom " ^ quote name, [theory]))
    1.15    end;
    1.16  
    1.17 -fun def_name c = c ^ "_def";
    1.18 -
    1.19 -fun def_name_optional c "" = def_name c
    1.20 -  | def_name_optional _ name = name;
    1.21 -
    1.22 -fun get_def thy = axiom thy o NameSpace.intern (Theory.axiom_space thy) o def_name;
    1.23 -
    1.24 -
    1.25  (*return additional axioms of this theory node*)
    1.26  fun axioms_of thy =
    1.27    map (fn s => (s, axiom thy s)) (Symtab.keys (Theory.axiom_table thy));