# HG changeset patch
# User wenzelm
# Date 1362664975 -3600
# Node ID 2ea5c7c2d8250742e55334e457ae48728d52427b
# Parent  4b5a5e26161d757f84f438e6236f4c35c14e59b7
tuned signature -- prefer terminology of Scala and Axiom;

diff -r 4b5a5e26161d -r 2ea5c7c2d825 src/Pure/Isar/code.ML
--- a/src/Pure/Isar/code.ML	Thu Mar 07 13:44:54 2013 +0100
+++ b/src/Pure/Isar/code.ML	Thu Mar 07 15:02:55 2013 +0100
@@ -90,8 +90,8 @@
 signature PRIVATE_CODE =
 sig
   include CODE
-  val declare_data: Object.T -> serial
-  val change_yield_data: serial * ('a -> Object.T) * (Object.T -> 'a)
+  val declare_data: Any.T -> serial
+  val change_yield_data: serial * ('a -> Any.T) * (Any.T -> 'a)
     -> theory -> ('a -> 'b * 'a) -> 'b * 'a
 end;
 
@@ -249,7 +249,7 @@
 
 local
 
-type kind = { empty: Object.T };
+type kind = { empty: Any.T };
 
 val kinds = Synchronized.var "Code_Data" (Datatab.empty: kind Datatab.table);
 
@@ -276,7 +276,7 @@
 
 local
 
-type data = Object.T Datatab.table;
+type data = Any.T Datatab.table;
 fun empty_dataref () = Synchronized.var "code data" (NONE : (data * theory_ref) option);
 
 structure Code_Data = Theory_Data
diff -r 4b5a5e26161d -r 2ea5c7c2d825 src/Pure/context.ML
--- a/src/Pure/context.ML	Thu Mar 07 13:44:54 2013 +0100
+++ b/src/Pure/context.ML	Thu Mar 07 15:02:55 2013 +0100
@@ -92,16 +92,16 @@
   include CONTEXT
   structure Theory_Data:
   sig
-    val declare: Position.T -> Object.T -> (Object.T -> Object.T) ->
-      (pretty -> Object.T * Object.T -> Object.T) -> serial
-    val get: serial -> (Object.T -> 'a) -> theory -> 'a
-    val put: serial -> ('a -> Object.T) -> 'a -> theory -> theory
+    val declare: Position.T -> Any.T -> (Any.T -> Any.T) ->
+      (pretty -> Any.T * Any.T -> Any.T) -> serial
+    val get: serial -> (Any.T -> 'a) -> theory -> 'a
+    val put: serial -> ('a -> Any.T) -> 'a -> theory -> theory
   end
   structure Proof_Data:
   sig
-    val declare: (theory -> Object.T) -> serial
-    val get: serial -> (Object.T -> 'a) -> Proof.context -> 'a
-    val put: serial -> ('a -> Object.T) -> 'a -> Proof.context -> Proof.context
+    val declare: (theory -> Any.T) -> serial
+    val get: serial -> (Any.T -> 'a) -> Proof.context -> 'a
+    val put: serial -> ('a -> Any.T) -> 'a -> Proof.context -> Proof.context
   end
 end;
 
@@ -119,15 +119,15 @@
 (*private copy avoids potential conflict of table exceptions*)
 structure Datatab = Table(type key = int val ord = int_ord);
 
-datatype pretty = Pretty of Object.T;
+datatype pretty = Pretty of Any.T;
 
 local
 
 type kind =
  {pos: Position.T,
-  empty: Object.T,
-  extend: Object.T -> Object.T,
-  merge: pretty -> Object.T * Object.T -> Object.T};
+  empty: Any.T,
+  extend: Any.T -> Any.T,
+  merge: pretty -> Any.T * Any.T -> Any.T};
 
 val kinds = Synchronized.var "Theory_Data" (Datatab.empty: kind Datatab.table);
 
@@ -170,7 +170,7 @@
     id: serial,                   (*identifier*)
     ids: unit Inttab.table} *     (*cumulative identifiers of non-drafts -- symbolic body content*)
    (*data*)
-   Object.T Datatab.table *       (*body content*)
+   Any.T Datatab.table *       (*body content*)
    (*ancestry*)
    {parents: theory list,         (*immediate predecessors*)
     ancestors: theory list} *     (*all predecessors -- canonical reverse order*)
@@ -464,7 +464,7 @@
 
 structure Proof =
 struct
-  datatype context = Context of Object.T Datatab.table * theory_ref;
+  datatype context = Context of Any.T Datatab.table * theory_ref;
 end;
 
 fun theory_of_proof (Proof.Context (_, thy_ref)) = deref thy_ref;
@@ -476,7 +476,7 @@
 
 local
 
-val kinds = Synchronized.var "Proof_Data" (Datatab.empty: (theory -> Object.T) Datatab.table);
+val kinds = Synchronized.var "Proof_Data" (Datatab.empty: (theory -> Any.T) Datatab.table);
 
 fun invoke_init k =
   (case Datatab.lookup (Synchronized.value kinds) k of
diff -r 4b5a5e26161d -r 2ea5c7c2d825 src/Pure/library.ML
--- a/src/Pure/library.ML	Thu Mar 07 13:44:54 2013 +0100
+++ b/src/Pure/library.ML	Thu Mar 07 15:02:55 2013 +0100
@@ -216,7 +216,7 @@
   val serial_string: unit -> string
   eqtype stamp
   val stamp: unit -> stamp
-  structure Object: sig type T = exn end
+  structure Any: sig type T = exn end
   val cd: string -> unit
   val pwd: unit -> string
   val getenv: string -> string
@@ -1065,11 +1065,11 @@
 fun stamp () = Stamp (serial ());
 
 
-(* generic objects *)
+(* values of any type *)
 
 (*note that the builtin exception datatype may be extended by new
   constructors at any time*)
-structure Object = struct type T = exn end;
+structure Any = struct type T = exn end;
 
 
 (* current directory *)