# HG changeset patch
# User wenzelm
# Date 1150405736 -7200
# Node ID b1d179e42713a84d55778b621996c43795a39f0e
# Parent  fe661eb3b0e75237a81d9bb97e87487e77992dba
added variable.ML;

diff -r fe661eb3b0e7 -r b1d179e42713 src/Pure/IsaMakefile
--- a/src/Pure/IsaMakefile	Thu Jun 15 23:08:54 2006 +0200
+++ b/src/Pure/IsaMakefile	Thu Jun 15 23:08:56 2006 +0200
@@ -66,7 +66,7 @@
   library.ML logic.ML meta_simplifier.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 unify.ML
+  type.ML type_infer.ML variable.ML unify.ML
 	@./mk
 
 
diff -r fe661eb3b0e7 -r b1d179e42713 src/Pure/ROOT.ML
--- a/src/Pure/ROOT.ML	Thu Jun 15 23:08:54 2006 +0200
+++ b/src/Pure/ROOT.ML	Thu Jun 15 23:08:56 2006 +0200
@@ -47,6 +47,7 @@
 use "pure_thy.ML";
 use "display.ML";
 use "drule.ML";
+use "variable.ML";
 use "tctical.ML";
 use "search.ML";
 use "meta_simplifier.ML";