(un)fold: ignore facts;

--- a/doc-src/IsarRef/generic.tex	Wed Sep 08 16:44:11 1999 +0200
+++ b/doc-src/IsarRef/generic.tex	Wed Sep 08 18:10:39 1999 +0200
@@ -46,7 +46,8 @@
   $rule$ (single step, involving facts) or $elim$ (multiple steps, see
   \S\ref{sec:classical-basic}).
 \item [$unfold~thms$ and $fold~thms$] expand and fold back again the given
-  meta-level definitions throughout all goals; facts may not be involved.
+  meta-level definitions throughout all goals; any facts provided are
+  \emph{ignored}.
 \item [$succeed$] yields a single (unchanged) result; it is the identify of
   the ``\texttt{,}'' method combinator.
 \item [$fail$] yields an empty result sequence; it is the identify of the

--- 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 *)