# 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";