# HG changeset patch
# User wenzelm
# Date 936807039 -7200
# Node ID 1ea137d3b5bf9b3d2e93f1256eff7f4be65fd326
# Parent  2a75abcf30e08bad9d0f9ad47786413892d4d46e
(un)fold: ignore facts;

diff -r 2a75abcf30e0 -r 1ea137d3b5bf doc-src/IsarRef/generic.tex
--- 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
diff -r 2a75abcf30e0 -r 1ea137d3b5bf src/Pure/Isar/method.ML
--- 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 *)