# HG changeset patch
# User wenzelm
# Date 1230678111 -3600
# Node ID bf99ccf71b7c2be1af91710d40f0f10c59d99322
# Parent  3ee4656b9e0c983dfb0ed8f8808fa18748c8fb5b
added old_term.ML;

diff -r 3ee4656b9e0c -r bf99ccf71b7c src/Pure/IsaMakefile
--- a/src/Pure/IsaMakefile	Wed Dec 31 00:01:07 2008 +0100
+++ b/src/Pure/IsaMakefile	Wed Dec 31 00:01:51 2008 +0100
@@ -80,10 +80,11 @@
   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 ../Tools/quickcheck.ML
+  old_goals.ML old_term.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			\
+  ../Tools/quickcheck.ML
 	@./mk
 
 
diff -r 3ee4656b9e0c -r bf99ccf71b7c src/Pure/ROOT.ML
--- a/src/Pure/ROOT.ML	Wed Dec 31 00:01:07 2008 +0100
+++ b/src/Pure/ROOT.ML	Wed Dec 31 00:01:51 2008 +0100
@@ -26,6 +26,7 @@
 use "name.ML";
 use "term.ML";
 use "term_subst.ML";
+use "old_term.ML";
 use "logic.ML";
 use "General/pretty.ML";
 use "context.ML";