src/Pure/theory.ML
changeset 16803 014090d1e64b
parent 16743 21dbff595bf6
child 16883 a89fafe1cbd8
     1.1 --- a/src/Pure/theory.ML	Wed Jul 13 16:07:23 2005 +0200
     1.2 +++ b/src/Pure/theory.ML	Wed Jul 13 16:07:24 2005 +0200
     1.3 @@ -179,7 +179,7 @@
     1.4  val axioms_of = Symtab.dest o #2 o #axioms o rep_theory;
     1.5  fun all_axioms_of thy = List.concat (map axioms_of (thy :: ancestors_of thy));
     1.6  
     1.7 -fun defs_of thy = (case rep_theory thy of {defs=D, ...} => D)
     1.8 +val defs_of = #defs o rep_theory;
     1.9  
    1.10  fun requires thy name what =
    1.11    if Context.exists_name name thy then ()