# HG changeset patch
# User wenzelm
# Date 1119462075 -7200
# Node ID 3e493fa130a35f60b3330e78cbd243d654085731
# Parent  d4de40568ab193af576029e1391b3b674d74a311
obsolete (see Pure/context.ML);

diff -r d4de40568ab1 -r 3e493fa130a3 src/Pure/General/object.ML
--- a/src/Pure/General/object.ML	Wed Jun 22 18:26:28 2005 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,42 +0,0 @@
-(*  Title:      Pure/General/object.ML
-    ID:         $Id$
-    Author:     Markus Wenzel, TU Muenchen
-
-Generic objects of arbitrary type -- fool the ML type system via
-exception constructors.
-*)
-
-signature OBJECT =
-sig
-  type T
-  type kind
-  val kind: string -> kind
-  val name_of_kind: kind -> string
-  val eq_kind: kind * kind -> bool
-  val kind_error: kind -> 'a
-end;
-
-structure Object: OBJECT =
-struct
-
-
-(* anytype values *)
-
-type T = exn;
-
-
-(* kinds *)
-
-datatype kind = Kind of string * stamp;
-
-fun kind name = Kind (name, stamp ());
-
-fun name_of_kind (Kind (name, _)) = name;
-
-fun eq_kind (Kind (_, s1), Kind (_, s2)) = s1 = s2;
-
-fun kind_error k =
-  error ("## RUNTIME TYPE ERROR ##\nFailed to access " ^ quote (name_of_kind k) ^ " object");
-
-
-end;
diff -r d4de40568ab1 -r 3e493fa130a3 src/Pure/Isar/ROOT.ML
--- a/src/Pure/Isar/ROOT.ML	Wed Jun 22 18:26:28 2005 +0200
+++ b/src/Pure/Isar/ROOT.ML	Wed Jun 22 19:41:15 2005 +0200
@@ -10,7 +10,6 @@
 use "auto_bind.ML";
 use "rule_cases.ML";
 use "proof_context.ML";
-use "proof_data.ML";
 use "context_rules.ML";
 use "args.ML";
 use "attrib.ML";
diff -r d4de40568ab1 -r 3e493fa130a3 src/Pure/Isar/proof_data.ML
--- a/src/Pure/Isar/proof_data.ML	Wed Jun 22 18:26:28 2005 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,48 +0,0 @@
-(*  Title:      Pure/Isar/proof_data.ML
-    ID:         $Id$
-    Author:     Markus Wenzel, TU Muenchen
-
-Type-safe interface for proof context data.
-*)
-
-signature PROOF_DATA_ARGS =
-sig
-  val name: string
-  type T
-  val init: theory -> T
-  val print: ProofContext.context -> T -> unit
-end;
-
-signature PROOF_DATA =
-sig
-  type T
-  val init: theory -> theory
-  val print: ProofContext.context -> unit
-  val get: ProofContext.context -> T
-  val put: T -> ProofContext.context -> ProofContext.context
-  val map: (T -> T) -> ProofContext.context -> ProofContext.context
-end;
-
-functor ProofDataFun(Args: PROOF_DATA_ARGS): PROOF_DATA =
-struct
-
-(*object kind kept private!*)
-val kind = Object.kind Args.name;
-
-type T = Args.T;
-exception Data of T;
-
-val init =
-  ProofContext.init_data kind
-    (Data o Args.init, fn ctxt => fn (Data x) => Args.print ctxt x);
-
-val print = ProofContext.print_data kind;
-val get = ProofContext.get_data kind (fn Data x => x);
-val put = ProofContext.put_data kind Data;
-fun map f ctxt = put (f (get ctxt)) ctxt;
-
-end;
-
-
-(*hide private data access functions*)
-structure ProofContext: PROOF_CONTEXT = ProofContext;