# HG changeset patch
# User wenzelm
# Date 1153867484 -7200
# Node ID 4c57e850e8d5ed5473ed2f99796941fac6c77f14
# Parent  eb529c6883ec8f0e55215947522cb95e997fd9c3
added Pure/subgoal.ML;

diff -r eb529c6883ec -r 4c57e850e8d5 src/Pure/IsaMakefile
--- a/src/Pure/IsaMakefile	Tue Jul 25 23:17:42 2006 +0200
+++ b/src/Pure/IsaMakefile	Wed Jul 26 00:44:44 2006 +0200
@@ -65,8 +65,8 @@
   display.ML drule.ML envir.ML fact_index.ML goal.ML install_pp.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
+  simplifier.ML sorts.ML subgoal.ML tactic.ML tctical.ML term.ML theory.ML	\
+  thm.ML type.ML type_infer.ML variable.ML unify.ML
 	@./mk
 
 
diff -r eb529c6883ec -r 4c57e850e8d5 src/Pure/ROOT.ML
--- a/src/Pure/ROOT.ML	Tue Jul 25 23:17:42 2006 +0200
+++ b/src/Pure/ROOT.ML	Wed Jul 26 00:44:44 2006 +0200
@@ -71,6 +71,7 @@
 
 (*the Isar system*)
 cd "Isar"; use "ROOT.ML"; cd "..";
+use "subgoal.ML";
 
 use "Proof/extraction.ML";