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