# HG changeset patch
# User wenzelm
# Date 1181685716 -7200
# Node ID 3069dade3eb47d2822231a564d7325a804f4a695
# Parent  356edb5eb1c4a85f448745a5938c97d7167ac9bc
added context_position.ML;

diff -r 356edb5eb1c4 -r 3069dade3eb4 src/Pure/IsaMakefile
--- a/src/Pure/IsaMakefile	Wed Jun 13 00:01:54 2007 +0200
+++ b/src/Pure/IsaMakefile	Wed Jun 13 00:01:56 2007 +0200
@@ -64,11 +64,12 @@
   Tools/codegen_serializer.ML Tools/codegen_thingol.ML Tools/invoke.ML		\
   Tools/nbe.ML Tools/nbe_codegen.ML Tools/nbe_eval.ML Tools/xml_syntax.ML 	\
   assumption.ML axclass.ML codegen.ML compress.ML conjunction.ML consts.ML 	\
-  context.ML conv.ML defs.ML display.ML drule.ML envir.ML fact_index.ML goal.ML	\
-  install_pp.ML library.ML logic.ML meta_simplifier.ML more_thm.ML morphism.ML 	\
-  name.ML net.ML old_goals.ML pattern.ML proofterm.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
+  context.ML context_position.ML conv.ML defs.ML display.ML drule.ML		\
+  envir.ML fact_index.ML goal.ML install_pp.ML library.ML logic.ML		\
+  meta_simplifier.ML more_thm.ML morphism.ML name.ML net.ML old_goals.ML	\
+  pattern.ML proofterm.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 356edb5eb1c4 -r 3069dade3eb4 src/Pure/ROOT.ML
--- a/src/Pure/ROOT.ML	Wed Jun 13 00:01:54 2007 +0200
+++ b/src/Pure/ROOT.ML	Wed Jun 13 00:01:56 2007 +0200
@@ -28,6 +28,7 @@
 use "sorts.ML";
 use "type.ML";
 use "context.ML";
+use "context_position.ML";
 use "compress.ML";
 use "type_infer.ML";