--- a/src/HOL/Univ.ML Mon Jul 24 23:51:11 2000 +0200
+++ b/src/HOL/Univ.ML Mon Jul 24 23:51:46 2000 +0200
@@ -387,7 +387,7 @@
by (Blast_tac 1);
qed "Funs_mono";
-val [p] = goalw thy [Funs_def] "(!!x. f x : S) ==> f : Funs S";
+val [p] = goalw (the_context ()) [Funs_def] "(!!x. f x : S) ==> f : Funs S";
by (rtac CollectI 1);
by (rtac subsetI 1);
by (etac rangeE 1);
@@ -401,7 +401,7 @@
by (rtac rangeI 1);
qed "FunsD";
-val [p1, p2] = goalw thy [o_def]
+val [p1, p2] = goalw (the_context ()) [o_def]
"[| f : Funs R; !!x. x : R ==> r (a x) = x |] ==> r o (a o f) = f";
by (rtac (p2 RS ext) 1);
by (rtac (p1 RS FunsD) 1);