src/HOL/Makefile

 	@if [ -d $${ISABELLEBIN:?}/Pure ];\
 		then echo Bad value for ISABELLEBIN: \
 			$(BIN) is the Isabelle source directory; \
 			exit 1; \
 	fi
-	@case `expr "//$(COMP)" : '[^ ]*/\(.*\)'` in \
+	@case `basename "$(COMP)"` in \
 	poly*)	echo 'make_database"$(BIN)/HOL"; quit();'  \
 		  | $(COMP) $(BIN)/Pure;\
 		if [ "$${MAKE_HTML}" = "true" ]; \
 		then echo 'open PolyML; make_html := true; exit_use_dir".";' \
 		       | $(COMP) $(BIN)/HOL;\

 	cd ../Pure;  $(MAKE)
 
 #### Testing of HOL
 
 #A macro referring to the object-logic (depends on ML compiler)
-LOGIC:sh=case `expr "//$ISABELLECOMP" : '[^ ]*/\(.*\)'` in \
-	poly*)	echo "$ISABELLECOMP $ISABELLEBIN/HOL" ;;\
-	sml*)	echo "$ISABELLEBIN/HOL" ;;\
+#	[Thanks to Thomas Santen and Stephan Herrmann from GMD First]
+LOGIC=`case \`basename "$(ISABELLECOMP)"\` in \
+	poly*)	echo "$(ISABELLECOMP) $(ISABELLEBIN)/HOL" ;;\
+	sml*)	echo "$(ISABELLEBIN)/HOL" ;;\
 	*)	echo "echo; echo Bad value for ISABELLECOMP: \
-			$ISABELLECOMP is not poly or sml; exit 1" ;;\
-	esac
+			$(ISABELLECOMP) is not poly or sml; exit 1" ;;\
+	esac`
 
 ##IMP-semantics example
 IMP_NAMES = Expr Com Natural Transition Denotation Hoare VC
 IMP_FILES = IMP/ROOT.ML $(IMP_NAMES:%=IMP/%.thy) $(IMP_NAMES:%=IMP/%.ML)
 

 	then echo 'make_html := true; exit_use_dir"Lex";quit();' | $(LOGIC);\
 	else echo 'exit_use_dir"Lex";quit();' | $(LOGIC); \
 	fi
 
 ##Miscellaneous examples
-EX_NAMES = String BT Perm Comb InSort Qsort LexProd Puzzle Mutil \
-	    Primes NatSum SList LList Acc PropLog Term Simult MT	    
+EX_NAMES = String BT Perm Comb InSort Qsort LexProd Group Ring Lagrange \
+	   Puzzle Mutil Primes NatSum SList LList Acc PropLog Term Simult MT
 
 EX_FILES = ex/ROOT.ML ex/cla.ML ex/meson.ML ex/mesontest.ML ex/rel.ML \
 	   ex/set.ML $(EX_NAMES:%=ex/%.thy) $(EX_NAMES:%=ex/%.ML)
 
 ex:	$(BIN)/HOL  $(EX_FILES)