# HG changeset patch
# User wenzelm
# Date 1222692082 -7200
# Node ID b906dd1de8553af44904bb51db74931d73cf9b94
# Parent  da9ae777451328f468f5f07bbfbdc5a36e425958
added context_position.ML;

diff -r da9ae7774513 -r b906dd1de855 src/Pure/IsaMakefile
--- a/src/Pure/IsaMakefile	Mon Sep 29 12:32:00 2008 +0200
+++ b/src/Pure/IsaMakefile	Mon Sep 29 14:41:22 2008 +0200
@@ -76,13 +76,14 @@
   Thy/thy_output.ML Tools/ROOT.ML Tools/invoke.ML Tools/quickcheck.ML	\
   Tools/value.ML Tools/isabelle_process.ML Tools/named_thms.ML		\
   Tools/xml_syntax.ML assumption.ML axclass.ML codegen.ML config.ML	\
-  conjunction.ML consts.ML context.ML conv.ML defs.ML display.ML	\
-  drule.ML envir.ML facts.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
+  conjunction.ML consts.ML context.ML context_position.ML conv.ML	\
+  defs.ML display.ML drule.ML envir.ML facts.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 da9ae7774513 -r b906dd1de855 src/Pure/ROOT.ML
--- a/src/Pure/ROOT.ML	Mon Sep 29 12:32:00 2008 +0200
+++ b/src/Pure/ROOT.ML	Mon Sep 29 14:41:22 2008 +0200
@@ -29,9 +29,10 @@
 use "term_subst.ML";
 use "logic.ML";
 use "General/pretty.ML";
+use "context.ML";
+use "context_position.ML";
 use "Syntax/lexicon.ML";
 use "Syntax/simple_syntax.ML";
-use "context.ML";
 use "sorts.ML";
 use "type.ML";
 use "config.ML";