# HG changeset patch
# User haftmann
# Date 1155799490 -7200
# Node ID 88cab786d0242c59f8b0670e7f22b5c25fe44903
# Parent  d079804d3b82d61b6d539859e594523c435ceb13
dropped definitions_of

diff -r d079804d3b82 -r 88cab786d024 src/Pure/theory.ML
--- a/src/Pure/theory.ML	Thu Aug 17 09:24:49 2006 +0200
+++ b/src/Pure/theory.ML	Thu Aug 17 09:24:50 2006 +0200
@@ -39,8 +39,6 @@
   val axioms_of: theory -> (string * term) list
   val all_axioms_of: theory -> (string * term) list
   val defs_of : theory -> Defs.T
-  val definitions_of: theory -> string ->
-    {module: string, name: string, lhs: typ, rhs: (string * typ) list} list
   val self_ref: theory -> theory_ref
   val deref: theory_ref -> theory
   val merge: theory * theory -> theory                     (*exception TERM*)
@@ -152,18 +150,6 @@
 
 val defs_of = #defs o rep_theory;
 
-fun definitions_of thy c =
-  let
-    val inst = Consts.instance (Sign.consts_of thy);
-    val defs = defs_of thy;
-  in
-    Defs.specifications_of defs c
-    |> map_filter (fn (_, {is_def, module, name, lhs, rhs}) =>
-      if is_def then SOME {module = module, name = name, lhs = inst (c, lhs),
-        rhs = map (fn (d, Us) => (d, inst (d, Us))) rhs}
-      else NONE)
-  end;
-
 fun requires thy name what =
   if Context.exists_name name thy then ()
   else error ("Require theory " ^ quote name ^ " as an ancestor for " ^ what);