# HG changeset patch
# User clasohm
# Date 795874962 -3600
# Node ID 6d36fe1bb234a5683de6a53f0b374424387d79b2
# Parent  b051e2fc2e340bb12e77793473a63d3d07cb9666
fixed bug: HOL_build_completed replaced by CHOL_build_completed

diff -r b051e2fc2e34 -r 6d36fe1bb234 src/HOL/ex/ROOT.ML
--- a/src/HOL/ex/ROOT.ML	Wed Mar 22 12:42:34 1995 +0100
+++ b/src/HOL/ex/ROOT.ML	Wed Mar 22 13:22:42 1995 +0100
@@ -1,4 +1,4 @@
-(*  Title:  	HOL/ex/ROOT
+(*  Title:  	CHOL/ex/ROOT
     ID:         $Id$
     Author: 	Tobias Nipkow, Cambridge University Computer Laboratory
     Copyright   1991  University of Cambridge
@@ -6,9 +6,9 @@
 Executes miscellaneous examples for Higher-Order Logic. 
 *)
 
-HOL_build_completed;    (*Cause examples to fail if HOL did*)
+CHOL_build_completed;    (*Cause examples to fail if CHOL did*)
 
-(writeln"Root file for HOL examples";
+(writeln"Root file for CHOL examples";
  proof_timing := true;
  loadpath := ["ex"];
  time_use     "ex/cla.ML";