# HG changeset patch
# User wenzelm
# Date 1138727972 -3600
# Node ID 2ee8333a2ba152979beb8d494a1326f8bda2887f
# Parent  ddb6803da1974ad929bbf88d49b8eba6f53e01b1
(un)fold: removed '(raw)' option;

diff -r ddb6803da197 -r 2ee8333a2ba1 src/Pure/Isar/method.ML
--- a/src/Pure/Isar/method.ML	Tue Jan 31 18:19:31 2006 +0100
+++ b/src/Pure/Isar/method.ML	Tue Jan 31 18:19:32 2006 +0100
@@ -35,8 +35,8 @@
   val cheating: bool -> ProofContext.context -> method
   val intro: thm list -> method
   val elim: thm list -> method
-  val unfold: bool -> thm list -> ProofContext.context -> method
-  val fold: bool -> thm list -> ProofContext.context -> method
+  val unfold: thm list -> ProofContext.context -> method
+  val fold: thm list -> ProofContext.context -> method
   val atomize: bool -> method
   val this: method
   val fact: thm list -> ProofContext.context -> method
@@ -193,8 +193,8 @@
 
 (* unfold/fold definitions *)
 
-fun unfold_meth b ths ctxt = SIMPLE_METHOD (CHANGED_PROP (LocalDefs.unfold_tac ctxt b ths));
-fun fold_meth b ths ctxt = SIMPLE_METHOD (CHANGED_PROP (LocalDefs.fold_tac ctxt b ths));
+fun unfold_meth ths ctxt = SIMPLE_METHOD (CHANGED_PROP (LocalDefs.unfold_tac ctxt ths));
+fun fold_meth ths ctxt = SIMPLE_METHOD (CHANGED_PROP (LocalDefs.fold_tac ctxt ths));
 
 
 (* atomize rule statements *)
@@ -650,13 +650,6 @@
 end;
 
 
-(* unfold syntax *)
-
-fun unfold_syntax m src =
-  syntax ((Args.mode "raw" >> not) -- Attrib.local_thmss) src
-  #> (fn (ctxt, (b, ths)) => m b ths ctxt);
-
-
 (* iprover syntax *)
 
 local
@@ -739,8 +732,8 @@
   ("insert", thms_args insert, "insert theorems, ignoring facts (improper)"),
   ("intro", thms_args intro, "repeatedly apply introduction rules"),
   ("elim", thms_args elim, "repeatedly apply elimination rules"),
-  ("unfold", unfold_syntax unfold_meth, "unfold definitions"),
-  ("fold", unfold_syntax fold_meth, "fold definitions"),
+  ("unfold", thms_ctxt_args unfold_meth, "unfold definitions"),
+  ("fold", thms_ctxt_args fold_meth, "fold definitions"),
   ("atomize", (atomize o #2) oo syntax (Args.mode "full"),
     "present local premises as object-level statements"),
   ("iprover", iprover_meth, "intuitionistic proof search"),