# HG changeset patch
# User haftmann
# Date 1186667574 -7200
# Node ID 8be734b5f59f932b9ae7da93ea4691977c09d5d4
# Parent  4031da6d8ba324c00bad0847bb05a42f10b6319c
new access interface in defs.ML

diff -r 4031da6d8ba3 -r 8be734b5f59f src/Pure/defs.ML
--- a/src/Pure/defs.ML	Thu Aug 09 15:52:53 2007 +0200
+++ b/src/Pure/defs.ML	Thu Aug 09 15:52:54 2007 +0200
@@ -11,14 +11,16 @@
   val pretty_const: Pretty.pp -> string * typ list -> Pretty.T
   val plain_args: typ list -> bool
   type T
-  val specifications_of: T -> string -> (serial * {is_def: bool, thyname: string, name: string,
-    lhs: typ list, rhs: (string * typ list) list}) list
+  val specifications_of: T -> string -> {is_def: bool, name: string,
+    lhs: typ list, rhs: (string * typ list) list} list
+  val all_specifications_of: T -> (string * {is_def: bool, name: string,
+    lhs: typ list, rhs: (string * typ list) list} list) list
   val dest: T ->
    {restricts: ((string * typ list) * string) list,
     reducts: ((string * typ list) * (string * typ list) list) list}
   val empty: T
   val merge: Pretty.pp -> T * T -> T
-  val define: Pretty.pp -> bool -> bool -> string -> string ->
+  val define: Pretty.pp -> bool -> bool -> string ->
     string * typ list -> (string * typ list) list -> T -> T
 end
 
@@ -51,7 +53,7 @@
 
 (* datatype defs *)
 
-type spec = {is_def: bool, thyname: string, name: string, lhs: args, rhs: (string * args) list};
+type spec = {is_def: bool, name: string, lhs: args, rhs: (string * args) list};
 
 type def =
  {specs: spec Inttab.table,                 (*source specifications*)
@@ -74,7 +76,9 @@
     SOME (def: def) => which def
   | NONE => []);
 
-fun specifications_of (Defs defs) = lookup_list (Inttab.dest o #specs) defs;
+fun specifications_of (Defs defs) = lookup_list (map snd o Inttab.dest o #specs) defs;
+fun all_specifications_of (Defs defs) =
+  ((map o apsnd) (map snd o Inttab.dest o #specs) o Symtab.dest) defs;
 val restricts_of = lookup_list #restricts;
 val reducts_of = lookup_list #reducts;
 
@@ -197,14 +201,14 @@
 
 (* define *)
 
-fun define pp unchecked is_def thyname name (c, args) deps (Defs defs) =
+fun define pp unchecked is_def name (c, args) deps (Defs defs) =
   let
     val restr =
       if plain_args args orelse
         (case args of [Type (a, rec_args)] => plain_args rec_args | _ => false)
       then [] else [(args, name)];
     val spec =
-      (serial (), {is_def = is_def, thyname = thyname, name = name, lhs = args, rhs = deps});
+      (serial (), {is_def = is_def, name = name, lhs = args, rhs = deps});
     val defs' = defs |> update_specs c spec;
   in Defs (defs' |> (if unchecked then I else dependencies pp (c, args) restr deps)) end;
 
diff -r 4031da6d8ba3 -r 8be734b5f59f src/Pure/theory.ML
--- a/src/Pure/theory.ML	Thu Aug 09 15:52:53 2007 +0200
+++ b/src/Pure/theory.ML	Thu Aug 09 15:52:54 2007 +0200
@@ -214,7 +214,7 @@
       else error ("Specification depends on extra type variables: " ^
         commas_quote (map (Pretty.string_of_typ pp o TFree) rhs_extras) ^
         "\nThe error(s) above occurred in " ^ quote name);
-  in Defs.define pp unchecked is_def (Context.theory_name thy) name (prep lhs) (map prep rhs) end;
+  in Defs.define pp unchecked is_def name (prep lhs) (map prep rhs) end;
 
 fun add_deps a raw_lhs raw_rhs thy =
   let