| changeset 7526 | 1ea137d3b5bf |
| parent 7506 | 08a88d4ebd54 |
| child 7555 | dd281afb33d7 |
--- a/src/Pure/Isar/method.ML Wed Sep 08 16:44:11 1999 +0200 +++ b/src/Pure/Isar/method.ML Wed Sep 08 18:10:39 1999 +0200 @@ -116,8 +116,8 @@ (* fold / unfold definitions *) -val fold = METHOD0 o fold_goals_tac; -val unfold = METHOD0 o rewrite_goals_tac; +fun fold thms = METHOD (fn _ => fold_goals_tac thms); +fun unfold thms = METHOD (fn _ => rewrite_goals_tac thms); (* multi_resolve *)