--- a/src/HOLCF/Fun2.ML Fri May 23 18:55:28 1997 +0200
+++ b/src/HOLCF/Fun2.ML Sun May 25 11:07:52 1997 +0200
@@ -12,7 +12,7 @@
qed_goal "inst_fun_po" thy "(op <<)=(%f g.!x.f x << g x)"
(fn prems =>
[
- (fold_goals_tac [po_def,less_fun_def]),
+ (fold_goals_tac [less_fun_def]),
(rtac refl 1)
]);