# HG changeset patch
# User wenzelm
# Date 1201215071 -3600
# Node ID 03937086b1fe454bc09714d1ad0bc1cd8a27e27f
# Parent  2152b47a87ed4a66918d8ea9da227ed47c0d5b59
removed obsolete context_position.ML (superseded by Position.thread_data);

diff -r 2152b47a87ed -r 03937086b1fe src/Pure/IsaMakefile
--- a/src/Pure/IsaMakefile	Thu Jan 24 12:02:44 2008 +0100
+++ b/src/Pure/IsaMakefile	Thu Jan 24 23:51:11 2008 +0100
@@ -70,13 +70,12 @@
   Tools/ROOT.ML Tools/invoke.ML Tools/isabelle_process.ML			\
   Tools/named_thms.ML Tools/xml_syntax.ML assumption.ML axclass.ML		\
   codegen.ML compress.ML config.ML conjunction.ML consts.ML context.ML		\
-  context_position.ML conv.ML defs.ML display.ML drule.ML envir.ML		\
-  fact_index.ML goal.ML interpretation.ML library.ML logic.ML			\
-  meta_simplifier.ML more_thm.ML morphism.ML name.ML net.ML old_goals.ML	\
-  pattern.ML primitive_defs.ML proofterm.ML pure_setup.ML pure_thy.ML		\
-  search.ML sign.ML simplifier.ML sorts.ML subgoal.ML tactic.ML			\
-  tctical.ML term.ML term_subst.ML theory.ML thm.ML type.ML			\
-  type_infer.ML unify.ML variable.ML
+  conv.ML defs.ML display.ML drule.ML envir.ML fact_index.ML goal.ML		\
+  interpretation.ML library.ML logic.ML meta_simplifier.ML more_thm.ML		\
+  morphism.ML name.ML net.ML old_goals.ML pattern.ML primitive_defs.ML		\
+  proofterm.ML pure_setup.ML pure_thy.ML search.ML sign.ML simplifier.ML	\
+  sorts.ML subgoal.ML tactic.ML tctical.ML term.ML term_subst.ML theory.ML	\
+  thm.ML type.ML type_infer.ML unify.ML variable.ML
 	@./mk
 
 
diff -r 2152b47a87ed -r 03937086b1fe src/Pure/ROOT.ML
--- a/src/Pure/ROOT.ML	Thu Jan 24 12:02:44 2008 +0100
+++ b/src/Pure/ROOT.ML	Thu Jan 24 23:51:11 2008 +0100
@@ -26,7 +26,6 @@
 use "Syntax/lexicon.ML";
 use "Syntax/simple_syntax.ML";
 use "context.ML";
-use "context_position.ML";
 use "sorts.ML";
 use "type.ML";
 use "type_infer.ML";
diff -r 2152b47a87ed -r 03937086b1fe src/Pure/context_position.ML
--- a/src/Pure/context_position.ML	Thu Jan 24 12:02:44 2008 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,35 +0,0 @@
-(*  Title:      Pure/context_position.ML
-    ID:         $Id$
-    Author:     Makarius
-
-Context positions.
-*)
-
-signature CONTEXT_POSITION =
-sig
-  val put: Position.T -> Context.generic -> Context.generic
-  val put_ctxt: Position.T -> Proof.context -> Proof.context
-  val get: Proof.context -> Position.T
-  val str_of: Proof.context -> string
-  val properties_of: Proof.context -> Markup.property list
-end;
-
-structure ContextPosition: CONTEXT_POSITION =
-struct
-
-structure Data = GenericDataFun
-(
-  type T = Position.T;
-  val empty = Position.none;
-  fun extend _ = empty;
-  fun merge _ _ = empty;
-);
-
-val put = Data.put;
-val put_ctxt = Context.proof_map o put;
-
-val get = Data.get o Context.Proof;
-val str_of = Position.str_of o get;
-val properties_of = Position.properties_of o get;
-
-end;