# HG changeset patch
# User paulson
# Date 845889514 -7200
# Node ID 292df12bace531ddaaa392d75ac6509b98983321
# Parent  73bbf2cc76513370d0d4784c4a7ed2eb85b5054c
ISABELLECOMP may now have a leading pathname

diff -r 73bbf2cc7651 -r 292df12bace5 src/CCL/Makefile
--- a/src/CCL/Makefile	Mon Oct 21 09:51:18 1996 +0200
+++ b/src/CCL/Makefile	Mon Oct 21 11:18:34 1996 +0200
@@ -34,7 +34,7 @@
 
 #Uses cp rather than make_database because Poly/ML allows only 3 levels
 $(BIN)/CCL:   $(BIN)/FOL  $(SET_FILES)	$(CCL_FILES) 
-	case "$(COMP)" in \
+	@case `expr "//$(COMP)" : '[^ ]*/\(.*\)'` in \
 	poly*)	cp $(BIN)/FOL $(BIN)/CCL;\
 		if [ "$${MAKE_HTML}" = "true" ]; \
 		then echo 'open PolyML; make_html := true; exit_use_dir".";' \
@@ -54,14 +54,14 @@
 		       | $(BIN)/FOL;\
 		fi;;\
 	*)	echo Bad value for ISABELLECOMP: \
-			$(COMP) is not poly or sml;;\
+			\"$(COMP)\" is not poly or sml;;\
 	esac
 
 $(BIN)/FOL:
 	cd ../FOL;  $(MAKE)
 
 test:	ex/ROOT.ML  $(BIN)/CCL	$(EX_FILES)
-	case "$(COMP)" in \
+	@case `expr "//$(COMP)" : '[^ ]*/\(.*\)'` in \
 	poly*)	if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
 		then echo 'make_html := true; exit_use_dir"ex"; quit();' \
 		       | $(COMP) $(BIN)/CCL;\
@@ -73,7 +73,7 @@
 		else echo 'exit_use_dir"ex";' | $(BIN)/CCL;\
 		fi;;\
 	*)	echo Bad value for ISABELLECOMP: \
-			$(COMP) is not poly or sml;;\
+			\"$(COMP)\" is not poly or sml;;\
 	esac
 
 .PRECIOUS:  $(BIN)/FOL $(BIN)/CCL 
diff -r 73bbf2cc7651 -r 292df12bace5 src/CTT/Makefile
--- a/src/CTT/Makefile	Mon Oct 21 09:51:18 1996 +0200
+++ b/src/CTT/Makefile	Mon Oct 21 11:18:34 1996 +0200
@@ -27,12 +27,12 @@
 EX_FILES = ex/ROOT.ML ex/elim.ML ex/equal.ML ex/synth.ML ex/typechk.ML
 
 $(BIN)/CTT:   $(BIN)/Pure  $(FILES) 
-	if [ -d $${ISABELLEBIN:?}/Pure ];\
+	@if [ -d $${ISABELLEBIN:?}/Pure ];\
 		then echo Bad value for ISABELLEBIN: \
 			$(BIN) is the Isabelle source directory; \
 			exit 1; \
-		fi;\
-	case "$(COMP)" in \
+	fi
+	@case `expr "//$(COMP)" : '[^ ]*/\(.*\)'` in \
 	poly*)	echo 'make_database"$(BIN)/CTT"; quit();'  \
 			| $(COMP) $(BIN)/Pure;\
 		if [ "$${MAKE_HTML}" = "true" ]; \
@@ -53,18 +53,18 @@
 		       | $(BIN)/Pure;\
 		fi;;\
 	*)	echo Bad value for ISABELLECOMP: \
-			$(COMP) is not poly or sml;;\
+			\"$(COMP)\" is not poly or sml;;\
 	esac
 
 $(BIN)/Pure:
 	cd ../Pure;  $(MAKE)
 
 test:	ex/ROOT.ML $(BIN)/CTT  $(EX_FILES) 
-	case "$(COMP)" in \
+	@case `expr "//$(COMP)" : '[^ ]*/\(.*\)'` in \
 	poly*)	echo 'exit_use"ex/ROOT.ML"; quit();' | $(COMP) $(BIN)/CTT ;;\
 	sml*)	echo 'exit_use"ex/ROOT.ML";' | $(BIN)/CTT;;\
 	*)	echo Bad value for ISABELLECOMP: \
-			$(COMP) is not poly or sml;;\
+			\"$(COMP)\" is not poly or sml;;\
 	esac
 
 .PRECIOUS:  $(BIN)/Pure	 $(BIN)/CTT 
diff -r 73bbf2cc7651 -r 292df12bace5 src/Cube/Makefile
--- a/src/Cube/Makefile	Mon Oct 21 09:51:18 1996 +0200
+++ b/src/Cube/Makefile	Mon Oct 21 11:18:34 1996 +0200
@@ -25,7 +25,7 @@
 FILES =		ROOT.ML	 Cube.thy  Cube.ML
 
 $(BIN)/Cube:   $(BIN)/Pure  $(FILES) 
-	case "$(COMP)" in \
+	@case `expr "//$(COMP)" : '[^ ]*/\(.*\)'` in \
 	poly*)	echo 'make_database"$(BIN)/Cube"; quit();'  \
 			| $(COMP) $(BIN)/Pure;\
 		if [ "$${MAKE_HTML}" = "true" ]; \
@@ -46,18 +46,18 @@
 		       | $(BIN)/Pure;\
 		fi;;\
 	*)	echo Bad value for ISABELLECOMP: \
-			$(COMP) is not poly or sml;;\
+			\"$(COMP)\" is not poly or sml;;\
 	esac
 
 $(BIN)/Pure:
 	cd ../Pure;  $(MAKE)
 
 test:	ex.ML $(BIN)/Cube
-	case "$(COMP)" in \
+	@case `expr "//$(COMP)" : '[^ ]*/\(.*\)'` in \
 	poly*)	echo 'exit_use"ex.ML"; quit();' | $(COMP) $(BIN)/Cube ;;\
 	sml*)	echo 'exit_use"ex.ML";' | $(BIN)/Cube;;\
 	*)	echo Bad value for ISABELLECOMP: \
-			$(COMP) is not poly or sml;;\
+			\"$(COMP)\" is not poly or sml;;\
 	esac
 
 .PRECIOUS:  $(BIN)/Pure	 $(BIN)/Cube 
diff -r 73bbf2cc7651 -r 292df12bace5 src/FOL/Makefile
--- a/src/FOL/Makefile	Mon Oct 21 09:51:18 1996 +0200
+++ b/src/FOL/Makefile	Mon Oct 21 11:18:34 1996 +0200
@@ -30,12 +30,12 @@
 	   ex/prop.ML ex/quant.ML $(EX_NAMES:%=ex/%.thy) $(EX_NAMES:%=ex/%.ML)
 
 $(BIN)/FOL:   $(BIN)/Pure  $(FILES) 
-	if [ -d $${ISABELLEBIN:?}/Pure ];\
+	@if [ -d $${ISABELLEBIN:?}/Pure ];\
 		then echo Bad value for ISABELLEBIN: \
 			$(BIN) is the Isabelle source directory; \
 			exit 1; \
-		fi;\
-	case "$(COMP)" in \
+	fi
+	@case `expr "//$(COMP)" : '[^ ]*/\(.*\)'` in \
 	poly*)	echo 'make_database"$(BIN)/FOL"; quit();' \
 		  | $(COMP) $(BIN)/Pure;\
 		if [ "$${MAKE_HTML}" = "true" ]; \
@@ -56,14 +56,14 @@
 		       | $(BIN)/Pure;\
 		fi;;\
 	*)	echo Bad value for ISABELLECOMP: \
-			$(COMP) is not poly or sml;;\
+			\"$(COMP)\" is not poly or sml;;\
 	esac
 
 $(BIN)/Pure:
 	cd ../Pure;  $(MAKE)
 
 test:	ex/ROOT.ML  $(BIN)/FOL	$(EX_FILES) 
-	case "$(COMP)" in \
+	@case `expr "//$(COMP)" : '[^ ]*/\(.*\)'` in \
 	poly*)	if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
 		then echo 'make_html := true; exit_use_dir"ex"; quit();' \
 		       | $(COMP) $(BIN)/FOL;\
@@ -75,7 +75,7 @@
 		else echo 'exit_use_dir"ex";' | $(BIN)/FOL;\
 		fi;;\
 	*)	echo Bad value for ISABELLECOMP: \
-			$(COMP) is not poly or sml;;\
+			\"$(COMP)\" is not poly or sml;;\
 	esac
 
 .PRECIOUS:   $(BIN)/Pure  $(BIN)/FOL 
diff -r 73bbf2cc7651 -r 292df12bace5 src/FOLP/Makefile
--- a/src/FOLP/Makefile	Mon Oct 21 09:51:18 1996 +0200
+++ b/src/FOLP/Makefile	Mon Oct 21 11:18:34 1996 +0200
@@ -29,7 +29,7 @@
 	   ex/prop.ML ex/quant.ML
 
 $(BIN)/FOLP:   $(BIN)/Pure  $(FILES) 
-	case "$(COMP)" in \
+	@case `expr "//$(COMP)" : '[^ ]*/\(.*\)'` in \
 	poly*)	echo 'make_database"$(BIN)/FOLP"; quit();'  \
 			| $(COMP) $(BIN)/Pure;\
 		if [ "$${MAKE_HTML}" = "true" ]; \
@@ -50,14 +50,14 @@
 		       | $(BIN)/Pure;\
 		fi;;\
 	*)	echo Bad value for ISABELLECOMP: \
-			$(COMP) is not poly or sml;;\
+			\"$(COMP)\" is not poly or sml;;\
 	esac
 
 $(BIN)/Pure:
 	cd ../Pure;  $(MAKE)
 
 test:	ex/ROOT.ML  $(BIN)/FOLP	 $(EX_FILES) 
-	case "$(COMP)" in \
+	@case `expr "//$(COMP)" : '[^ ]*/\(.*\)'` in \
 	poly*)	if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
 		then echo 'make_html := true; exit_use_dir"ex"; quit();' \
 		       | $(COMP) $(BIN)/FOLP;\
@@ -69,7 +69,7 @@
 		else echo 'exit_use_dir"ex";' | $(BIN)/FOLP;\
 		fi;;\
 	*)	echo Bad value for ISABELLECOMP: \
-			$(COMP) is not poly or sml;;\
+			\"$(COMP)\" is not poly or sml;;\
 	esac
 
 .PRECIOUS:   $(BIN)/Pure  $(BIN)/FOLP 
diff -r 73bbf2cc7651 -r 292df12bace5 src/HOL/Makefile
--- a/src/HOL/Makefile	Mon Oct 21 09:51:18 1996 +0200
+++ b/src/HOL/Makefile	Mon Oct 21 11:18:34 1996 +0200
@@ -33,12 +33,12 @@
 	$(NAMES:%=%.thy) $(NAMES:%=%.ML)
 
 $(BIN)/HOL:   $(BIN)/Pure  $(FILES) 
-	if [ -d $${ISABELLEBIN:?}/Pure ];\
+	@if [ -d $${ISABELLEBIN:?}/Pure ];\
 		then echo Bad value for ISABELLEBIN: \
 			$(BIN) is the Isabelle source directory; \
 			exit 1; \
-		fi;\
-	case "$(COMP)" in \
+	fi
+	@case `expr "//$(COMP)" : '[^ ]*/\(.*\)'` in \
 	poly*)	echo 'make_database"$(BIN)/HOL"; quit();'  \
 		  | $(COMP) $(BIN)/Pure;\
 		if [ "$${MAKE_HTML}" = "true" ]; \
@@ -59,7 +59,7 @@
 		       | $(BIN)/Pure;\
 		fi;;\
 	*)	echo Bad value for ISABELLECOMP: \
-			$(COMP) is not poly or sml; exit 1;;\
+			\"$(COMP)\" is not poly or sml; exit 1;;\
 	esac
 
 $(BIN)/Pure:
@@ -68,11 +68,11 @@
 #### Testing of HOL
 
 #A macro referring to the object-logic (depends on ML compiler)
-LOGIC:sh=case $ISABELLECOMP in \
+LOGIC:sh=case `expr "//$ISABELLECOMP" : '[^ ]*/\(.*\)'` in \
 	poly*)	echo "$ISABELLECOMP $ISABELLEBIN/HOL" ;;\
 	sml*)	echo "$ISABELLEBIN/HOL" ;;\
-	*)	echo "echo Bad value for ISABELLECOMP: \
-			$ISABELLEBIN is not poly or sml; exit 1" ;;\
+	*)	echo "echo; echo Bad value for ISABELLECOMP: \
+			$ISABELLECOMP is not poly or sml; exit 1" ;;\
 	esac
 
 ##IMP-semantics example
@@ -80,7 +80,7 @@
 IMP_FILES = IMP/ROOT.ML $(IMP_NAMES:%=IMP/%.thy) $(IMP_NAMES:%=IMP/%.ML)
 
 IMP:	$(BIN)/HOL  $(IMP_FILES)
-	if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
+	@if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
 	then echo 'make_html := true; exit_use_dir"IMP";quit();' | $(LOGIC); \
 	else echo 'exit_use_dir"IMP";quit();' | $(LOGIC); \
 	fi
@@ -91,7 +91,7 @@
 	      $(Hoare_NAMES:%=Hoare/%.ML)
 
 Hoare:	$(BIN)/HOL  $(Hoare_FILES)
-	if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
+	@if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
 	then echo 'make_html := true; exit_use_dir"Hoare";quit();' | $(LOGIC);\
 	else echo 'exit_use_dir"Hoare";quit();' | $(LOGIC); \
 	fi
@@ -103,7 +103,7 @@
 	      $(INTEG_NAMES:%=Integ/%.thy) $(INTEG_NAMES:%=Integ/%.ML)
 
 Integ:	$(BIN)/HOL  $(INTEG_FILES)
-	if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
+	@if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
 	then echo 'make_html := true; exit_use_dir"Integ";quit();' | $(LOGIC);\
 	else echo 'exit_use_dir"Integ";quit();' | $(LOGIC); \
 	fi
@@ -123,7 +123,7 @@
  $(IOA_MT_NAMES:%=IOA/meta_theory/%.thy) $(IOA_MT_NAMES:%=IOA/meta_theory/%.ML)
 
 IOA:	$(BIN)/HOL  $(IOA_FILES)
-	if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
+	@if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
 	then echo 'make_html := true; exit_use_dir"IOA/NTP";quit();' \
 	       | $(LOGIC);\
 	     echo 'make_html := true; exit_use_dir"IOA/ABP";quit();' \
@@ -134,12 +134,13 @@
 
 
 ##Authentication & Security Protocols
-Auth_NAMES = Message Shared NS_Shared OtwayRees OtwayRees_AN Yahalom
+Auth_NAMES = Message Shared NS_Shared OtwayRees OtwayRees_AN OtwayRees_Bad \
+	     Yahalom Yahalom2
 
 AUTH_FILES = Auth/ROOT.ML $(AUTH_NAMES:%=Auth/%.thy) $(AUTH_NAMES:%=Auth/%.ML)
 
 Auth:	$(BIN)/HOL  $(AUTH_FILES)
-	if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
+	@if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
 	then echo 'make_html := true; exit_use_dir"Auth";quit();' | $(LOGIC);\
 	else echo 'exit_use_dir"Auth";quit();' | $(LOGIC); \
 	fi
@@ -152,7 +153,7 @@
 	      $(SUBST_NAMES:%=Subst/%.thy) $(SUBST_NAMES:%=Subst/%.ML)
 
 Subst:	$(BIN)/HOL  $(SUBST_FILES)
-	if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
+	@if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
 	then echo 'make_html := true; exit_use_dir"Subst";quit();' | $(LOGIC);\
 	else echo 'exit_use_dir"Subst";quit();' | $(LOGIC); \
 	fi
@@ -164,7 +165,7 @@
 	      $(LAMBDA_NAMES:%=Lambda/%.thy) $(LAMBDA_NAMES:%=Lambda/%.ML)
 
 Lambda:	 $(BIN)/HOL $(LAMBDA_FILES)
-	if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
+	@if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
 	then echo 'make_html := true; exit_use_dir"Lambda";quit();' \
 	       | $(LOGIC);\
 	else echo 'exit_use_dir"Lambda";quit();' | $(LOGIC); \
@@ -177,7 +178,7 @@
 	      $(MINIML_NAMES:%=MiniML/%.thy) $(MINIML_NAMES:%=MiniML/%.ML)
 
 MiniML: $(BIN)/HOL  $(MINIML_FILES)
-	if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
+	@if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
 	then echo 'make_html := true; exit_use_dir"MiniML";quit();' \
 	       | $(LOGIC);\
 	else echo 'exit_use_dir"MiniML";quit();' | $(LOGIC); \
@@ -190,7 +191,7 @@
 	    $(LEX_NAMES:%=Lex/%.thy) $(LEX_NAMES:%=Lex/%.ML)
 
 Lex:	$(BIN)/HOL  $(LEX_FILES)
-	if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
+	@if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
 	then echo 'make_html := true; exit_use_dir"Lex";quit();' | $(LOGIC);\
 	else echo 'exit_use_dir"Lex";quit();' | $(LOGIC); \
 	fi
@@ -203,7 +204,7 @@
 	   ex/set.ML $(EX_NAMES:%=ex/%.thy) $(EX_NAMES:%=ex/%.ML)
 
 ex:	$(BIN)/HOL  $(EX_FILES)
-	if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
+	@if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
 	then echo 'make_html := true; exit_use_dir"ex";quit();' | $(LOGIC);\
 	else echo 'exit_use_dir"ex";quit();' | $(LOGIC); \
 	fi
diff -r 73bbf2cc7651 -r 292df12bace5 src/HOLCF/Makefile
--- a/src/HOLCF/Makefile	Mon Oct 21 09:51:18 1996 +0200
+++ b/src/HOLCF/Makefile	Mon Oct 21 11:18:34 1996 +0200
@@ -34,7 +34,7 @@
 
 #Uses cp rather than make_database because Poly/ML allows only 3 levels
 $(BIN)/HOLCF:	$(BIN)/HOL  $(FILES) 
-	case "$(COMP)" in \
+	@case `expr "//$(COMP)" : '[^ ]*/\(.*\)'` in \
 	poly*)	cp $(BIN)/HOL $(BIN)/HOLCF; chmod u+w $(BIN)/HOLCF;\
 		if [ "$${MAKE_HTML}" = "true" ]; \
 		then echo 'open PolyML; make_html := true; exit_use_dir".";' \
@@ -54,7 +54,7 @@
 		       | $(BIN)/HOL;\
 		fi;;\
 	*)	echo Bad value for ISABELLECOMP: \
-			$(COMP) is not poly or sml;;\
+			\"$(COMP)\" is not poly or sml;;\
 	esac
 
 $(BIN)/HOL:
@@ -66,7 +66,7 @@
 EX_FILES = ex/ROOT.ML ex/loeckx.ML $(EX_THYS) $(EX_THYS:.thy=.ML)
 
 test:	ex/ROOT.ML  $(BIN)/HOLCF  $(EX_FILES) 
-	case "$(COMP)" in \
+	@case `expr "//$(COMP)" : '[^ ]*/\(.*\)'` in \
 	poly*)	if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
 		then echo 'make_html := true; exit_use_dir"ex"; quit();' \
 		       | $(COMP) $(BIN)/HOLCF;\
@@ -78,7 +78,7 @@
 		else echo 'exit_use_dir"ex";' | $(BIN)/HOLCF;\
 		fi;;\
 	*)	echo Bad value for ISABELLECOMP: \
-			$(COMP) is not poly or sml;;\
+			\"$(COMP)\" is not poly or sml;;\
 	esac
 
 EXPLICIT_DOMAINS_THYS = explicit_domains/Coind.thy explicit_domains/Dlist.thy \
@@ -90,7 +90,7 @@
 			 $(EXPLICIT_DOMAINS_THYS:.thy=.ML)
 
 test2:	explicit_domains/ROOT.ML  $(BIN)/HOLCF	$(EXPLICIT_DOMAINS_FILES) 
-	case "$(COMP)" in \
+	@case `expr "//$(COMP)" : '[^ ]*/\(.*\)'` in \
 	poly*)	if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
 		then echo 'make_html := true; exit_use_dir"explicit_domains";				  quit();' | $(COMP) $(BIN)/HOLCF;\
 		else echo 'exit_use_dir"explicit_domains"; quit();' \
@@ -102,7 +102,7 @@
 		else echo 'exit_use_dir"explicit_domains";' | $(BIN)/HOLCF;\
 		fi;;\
 	*)	echo Bad value for ISABELLECOMP: \
-			$(COMP) is not poly or sml;;\
+			\"$(COMP)\" is not poly or sml;;\
 	esac
 
 .PRECIOUS:  $(BIN)/HOL	$(BIN)/HOLCF 
diff -r 73bbf2cc7651 -r 292df12bace5 src/LCF/Makefile
--- a/src/LCF/Makefile	Mon Oct 21 09:51:18 1996 +0200
+++ b/src/LCF/Makefile	Mon Oct 21 11:18:34 1996 +0200
@@ -25,7 +25,7 @@
 
 #Uses cp rather than make_database because Poly/ML allows only 3 levels
 $(BIN)/LCF:   $(BIN)/FOL  $(FILES) 
-	case "$(COMP)" in \
+	@case `expr "//$(COMP)" : '[^ ]*/\(.*\)'` in \
 	poly*)	cp $(BIN)/FOL $(BIN)/LCF;\
 		if [ "$${MAKE_HTML}" = "true" ]; \
 		then echo 'open PolyML; make_html := true; exit_use_dir".";' \
@@ -45,18 +45,18 @@
 		       | $(BIN)/FOL;\
 		fi;;\
 	*)	echo Bad value for ISABELLECOMP: \
-			$(COMP) is not poly or sml;;\
+			\"$(COMP)\" is not poly or sml;;\
 	esac
 
 (BIN)/FOL:
 	cd ../FOL;  $(MAKE)
 
 test:	ex.ML  $(BIN)/LCF
-	case "$(COMP)" in \
+	@case `expr "//$(COMP)" : '[^ ]*/\(.*\)'` in \
 	poly*)	echo 'exit_use"ex.ML"; quit();' | $(COMP) $(BIN)/LCF ;;\
 	sml*)	echo 'exit_use"ex.ML";' | $(BIN)/LCF;;\
 	*)	echo Bad value for ISABELLECOMP: \
-			$(COMP) is not poly or sml;;\
+			\"$(COMP)\" is not poly or sml;;\
 	esac
 
 .PRECIOUS:   $(BIN)/FOL	 $(BIN)/LCF 
diff -r 73bbf2cc7651 -r 292df12bace5 src/Pure/Makefile
--- a/src/Pure/Makefile	Mon Oct 21 09:51:18 1996 +0200
+++ b/src/Pure/Makefile	Mon Oct 21 11:18:34 1996 +0200
@@ -37,7 +37,7 @@
 
 #Uses cp rather than make_database because Poly/ML allows only 3 levels
 $(BIN)/Pure:   $(FILES)	 $(SYNTAX_FILES)  $(THY_FILES)	$(ML_DBASE)
-	case "$(COMP)" in \
+	@case `expr "//$(COMP)" : '[^ ]*/\(.*\)'` in \
 	poly*)	echo database=$${ML_DBASE:?'No Poly/ML database specified'};\
 		cp $(ML_DBASE) $(BIN)/Pure; chmod u+w $(BIN)/Pure;\
 		echo 'PolyML.use"POLY";use"ROOT" handle _=> exit 1;' \
@@ -50,7 +50,7 @@
 		fi;\
 		echo 'use"NJ.ML"; use"ROOT.ML" handle _=> exit 1;				     xML"$(BIN)/Pure" banner;' | $(COMP);;\
 	*)	echo Bad value for ISABELLECOMP: \
-			$(COMP) is not poly or sml;;\
+			\"$(COMP)\" is not poly or sml;;\
 	esac
 
 
diff -r 73bbf2cc7651 -r 292df12bace5 src/Sequents/Makefile
--- a/src/Sequents/Makefile	Mon Oct 21 09:51:18 1996 +0200
+++ b/src/Sequents/Makefile	Mon Oct 21 11:18:34 1996 +0200
@@ -32,7 +32,7 @@
     $(ILL_NAMES:%=ex/ILL/%.thy) $(ILL_NAMES:%=ex/ILL/%.ML)
 
 $(BIN)/Sequents:   $(BIN)/Pure	$(FILES) 
-	case "$(COMP)" in \
+	@case `expr "//$(COMP)" : '[^ ]*/\(.*\)'` in \
 	poly*)	echo 'make_database"$(BIN)/Sequents"; quit();'	\
 			| $(COMP) $(BIN)/Pure;\
 		if [ "$${MAKE_HTML}" = "true" ]; \
@@ -52,18 +52,18 @@
 		       | $(BIN)/Pure;\
 		fi;;\
 	*)	echo Bad value for ISABELLECOMP: \
-			$(COMP) is not poly or sml;;\
+			\"$(COMP)\" is not poly or sml;;\
 	esac
 
 $(BIN)/Pure:
 	cd ../Pure;  $(MAKE)
 
 test:	$(BIN)/Sequents	 $(EX_FILES)
-	case "$(COMP)" in \
+	@case `expr "//$(COMP)" : '[^ ]*/\(.*\)'` in \
 	poly*)	echo 'exit_use"ex/ROOT.ML";quit();' | $(COMP) $(BIN)/Sequents;;\
 	sml*)	echo 'exit_use"ex/ROOT.ML";' | $(BIN)/Sequents;;\
 	*)	echo Bad value for ISABELLECOMP: \
-			$(COMP) is not poly or sml;;\
+			\"$(COMP)\" is not poly or sml;;\
 	esac
 
 
diff -r 73bbf2cc7651 -r 292df12bace5 src/ZF/Makefile
--- a/src/ZF/Makefile	Mon Oct 21 09:51:18 1996 +0200
+++ b/src/ZF/Makefile	Mon Oct 21 11:18:34 1996 +0200
@@ -35,7 +35,7 @@
 
 #Uses cp rather than make_database because Poly/ML allows only 3 levels
 $(BIN)/ZF:   $(BIN)/FOL	 $(FILES) 
-	case "$(COMP)" in \
+	@case `expr "//$(COMP)" : '[^ ]*/\(.*\)'` in \
 	poly*)	cp $(BIN)/FOL $(BIN)/ZF;\
 		if [ "$${MAKE_HTML}" = "true" ]; \
 		then echo 'open PolyML; make_html := true; exit_use_dir".";' \
@@ -55,7 +55,7 @@
 		       | $(BIN)/FOL;\
 		fi;;\
 	*)	echo Bad value for ISABELLECOMP: \
-			$(COMP) is not poly or sml; exit 1;;\
+			\"$(COMP)\" is not poly or sml; exit 1;;\
 	esac
 
 $(BIN)/FOL:
@@ -64,11 +64,11 @@
 #### Testing of ZF
 
 #A macro referring to the object-logic (depends on ML compiler)
-LOGIC:sh=case $ISABELLECOMP in \
+LOGIC:sh=case `expr "//$ISABELLECOMP" : '[^ ]*/\(.*\)'` in \
 	poly*)	echo "$ISABELLECOMP $ISABELLEBIN/ZF" ;;\
 	sml*)	echo "$ISABELLEBIN/ZF" ;;\
-	*)	echo "echo Bad value for ISABELLECOMP: \
-			$ISABELLEBIN is not poly or sml; exit 1" ;;\
+	*)	echo "echo; echo Bad value for ISABELLECOMP: \
+			$ISABELLECOMP is not poly or sml; exit 1" ;;\
 	esac
 
 ##IMP-semantics example
@@ -76,7 +76,7 @@
 IMP_FILES = IMP/ROOT.ML $(IMP_NAMES:%=IMP/%.thy) $(IMP_NAMES:%=IMP/%.ML)
 
 IMP:   $(BIN)/ZF  $(IMP_FILES)
-	if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
+	@if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
 	then echo 'make_html := true; exit_use_dir"IMP";quit();' | $(LOGIC); \
 	else echo 'exit_use_dir"IMP";quit();' | $(LOGIC); \
 	fi
@@ -88,7 +88,7 @@
 	      $(COIND_NAMES:%=Coind/%.thy) $(COIND_NAMES:%=Coind/%.ML)
 
 Coind:	$(BIN)/ZF  $(COIND_FILES)
-	if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
+	@if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
 	then echo 'make_html := true; exit_use_dir"Coind";quit();' | $(LOGIC);\
 	else echo 'exit_use_dir"Coind";quit();' | $(LOGIC); \
 	fi
@@ -105,7 +105,7 @@
 	   $(AC_NAMES:%=AC/%.thy) $(AC_NAMES:%=AC/%.ML)
 
 AC:  $(BIN)/ZF	$(AC_FILES)
-	if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
+	@if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
 	then echo 'make_html := true; exit_use_dir"AC";quit();' | $(LOGIC); \
 	else echo 'exit_use_dir"AC";quit();' | $(LOGIC); \
 	fi
@@ -119,7 +119,7 @@
 			    $(RESID_NAMES:%=Resid/%.ML)
 
 Resid:	$(BIN)/ZF  $(RESID_FILES)
-	if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
+	@if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
 	then echo 'make_html := true; exit_use_dir"Resid";quit();' | $(LOGIC);\
 	else echo 'exit_use_dir"Resid";quit();' | $(LOGIC); \
 	fi
@@ -132,7 +132,7 @@
 
 #Test ZF by loading the examples in directory ex
 ex:	$(BIN)/ZF  $(EX_FILES)
-	if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
+	@if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
 	then echo 'make_html := true; exit_use_dir"ex";quit();' | $(LOGIC); \
 	else echo 'exit_use_dir"ex";quit();' | $(LOGIC); \
 	fi