# HG changeset patch
# User nipkow
# Date 853842568 -3600
# Node ID 7a876fc091d67ff6804eefc1ac7a564cac631535
# Parent  2d5604a515621c8fe97bc0085148942c04a35330
Modified MiniML. Added W0.

diff -r 2d5604a51562 -r 7a876fc091d6 src/HOL/Makefile
--- a/src/HOL/Makefile	Tue Jan 21 10:58:32 1997 +0100
+++ b/src/HOL/Makefile	Tue Jan 21 11:29:28 1997 +0100
@@ -183,8 +183,23 @@
 	else echo 'exit_use_dir"Lambda";quit();' | $(LOGIC); \
 	fi
 
-##Type inference for MiniML
-MINIML_NAMES = I Maybe MiniML Type W
+## Type inference without let
+
+W0_NAMES = I Maybe MiniML Type W
+
+W0_FILES = W0/ROOT.ML \
+	      $(W0_NAMES:%=W0/%.thy) $(W0_NAMES:%=W0/%.ML)
+
+W0:	$(BIN)/HOL  $(W0_FILES)
+	@if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
+	then echo 'make_html := true; exit_use_dir"W0";quit();' \
+	       | $(LOGIC);\
+	else echo 'exit_use_dir"W0";quit();' | $(LOGIC); \
+	fi
+
+## Type inference with let
+
+MINIML_NAMES = Generalize Instance Maybe MiniML Type W
 
 MINIML_FILES = MiniML/ROOT.ML \
 	      $(MINIML_NAMES:%=MiniML/%.thy) $(MINIML_NAMES:%=MiniML/%.ML)