# HG changeset patch
# User wenzelm
# Date 1152613020 -7200
# Node ID a7e183bfebefeac84d5fdb4bd163f3cc6246d745
# Parent  b4d0b545df01e3f9067767bdba8362fcd2639d19
added name.ML;

diff -r b4d0b545df01 -r a7e183bfebef src/Pure/IsaMakefile
--- a/src/Pure/IsaMakefile	Tue Jul 11 12:16:59 2006 +0200
+++ b/src/Pure/IsaMakefile	Tue Jul 11 12:17:00 2006 +0200
@@ -63,7 +63,7 @@
   Tools/invoke.ML Tools/nbe.ML Tools/nbe_codegen.ML Tools/nbe_eval.ML		\
   axclass.ML codegen.ML compress.ML conjunction.ML consts.ML context.ML defs.ML	\
   display.ML drule.ML envir.ML fact_index.ML goal.ML install_pp.ML		\
-  library.ML logic.ML meta_simplifier.ML net.ML old_goals.ML pattern.ML		\
+  library.ML logic.ML meta_simplifier.ML name.ML net.ML old_goals.ML pattern.ML	\
   proof_general.ML proofterm.ML pure_thy.ML search.ML sign.ML			\
   simplifier.ML sorts.ML tactic.ML tctical.ML term.ML theory.ML thm.ML		\
   type.ML type_infer.ML variable.ML unify.ML
diff -r b4d0b545df01 -r a7e183bfebef src/Pure/ROOT.ML
--- a/src/Pure/ROOT.ML	Tue Jul 11 12:16:59 2006 +0200
+++ b/src/Pure/ROOT.ML	Tue Jul 11 12:17:00 2006 +0200
@@ -20,6 +20,7 @@
 cd "General"; use "ROOT.ML"; cd "..";
 
 (*fundamental structures*)
+use "name.ML";
 use "term.ML";
 use "General/pretty.ML";
 use "sorts.ML";