src/LCF/ex/Ex1.ML

--- a/src/LCF/ex/Ex1.ML	Sat Jun 20 20:35:38 1998 +0200
+++ b/src/LCF/ex/Ex1.ML	Mon Jun 22 15:09:59 1998 +0200
@@ -15,7 +15,7 @@
 bind_thm ("H_strict", H_strict);
 Addsimps [H_strict];
 
-goal thy "ALL x. H(FIX(K,x)) = FIX(K,x)";
+Goal "ALL x. H(FIX(K,x)) = FIX(K,x)";
 by (induct_tac "K" 1);
 by (Simp_tac 1);
 by (simp_tac (simpset() setloop (split_tac [COND_cases_iff])) 1);