dropped definitions_of
authorhaftmann
Thu Aug 17 09:24:50 2006 +0200 (2006-08-17)
changeset 2039288cab786d024
parent 20391 d079804d3b82
child 20393 df3252bbc0e6
dropped definitions_of
src/Pure/theory.ML
     1.1 --- a/src/Pure/theory.ML	Thu Aug 17 09:24:49 2006 +0200
     1.2 +++ b/src/Pure/theory.ML	Thu Aug 17 09:24:50 2006 +0200
     1.3 @@ -39,8 +39,6 @@
     1.4    val axioms_of: theory -> (string * term) list
     1.5    val all_axioms_of: theory -> (string * term) list
     1.6    val defs_of : theory -> Defs.T
     1.7 -  val definitions_of: theory -> string ->
     1.8 -    {module: string, name: string, lhs: typ, rhs: (string * typ) list} list
     1.9    val self_ref: theory -> theory_ref
    1.10    val deref: theory_ref -> theory
    1.11    val merge: theory * theory -> theory                     (*exception TERM*)
    1.12 @@ -152,18 +150,6 @@
    1.13  
    1.14  val defs_of = #defs o rep_theory;
    1.15  
    1.16 -fun definitions_of thy c =
    1.17 -  let
    1.18 -    val inst = Consts.instance (Sign.consts_of thy);
    1.19 -    val defs = defs_of thy;
    1.20 -  in
    1.21 -    Defs.specifications_of defs c
    1.22 -    |> map_filter (fn (_, {is_def, module, name, lhs, rhs}) =>
    1.23 -      if is_def then SOME {module = module, name = name, lhs = inst (c, lhs),
    1.24 -        rhs = map (fn (d, Us) => (d, inst (d, Us))) rhs}
    1.25 -      else NONE)
    1.26 -  end;
    1.27 -
    1.28  fun requires thy name what =
    1.29    if Context.exists_name name thy then ()
    1.30    else error ("Require theory " ^ quote name ^ " as an ancestor for " ^ what);