src/ZF/ZF.ML

--- a/src/ZF/ZF.ML	Mon Jun 22 15:53:24 1998 +0200
+++ b/src/ZF/ZF.ML	Mon Jun 22 17:12:27 1998 +0200
@@ -9,7 +9,7 @@
 open ZF;
 
 (*Useful examples:  singletonI RS subst_elem,  subst_elem RSN (2,IntI) *)
-goal ZF.thy "!!a b A. [| b:A;  a=b |] ==> a:A";
+Goal "!!a b A. [| b:A;  a=b |] ==> a:A";
 by (etac ssubst 1);
 by (assume_tac 1);
 val subst_elem = result();
@@ -271,7 +271,7 @@
     "b : {f(x). x:A} <-> (EX x:A. b=f(x))"
  (fn _ => [Blast_tac 1]);
 
-goal ZF.thy "{x. x:A} = A";
+Goal "{x. x:A} = A";
 by (Blast_tac 1);
 qed "triv_RepFun";