--- 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
--- 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
--- 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 *)