# HG changeset patch
# User wenzelm
# Date 1182287757 -7200
# Node ID b74315510f85dcffe61d3871f8be1552bad005bd
# Parent  d0580634f128624bd8e4e1293125d201013f7b29
added raw_tactic;

diff -r d0580634f128 -r b74315510f85 src/Pure/Isar/method.ML
--- a/src/Pure/Isar/method.ML	Tue Jun 19 23:15:54 2007 +0200
+++ b/src/Pure/Isar/method.ML	Tue Jun 19 23:15:57 2007 +0200
@@ -343,11 +343,14 @@
 val tactic_ref = ref ((fn _ => raise Match): Proof.context -> thm list -> tactic);
 fun set_tactic f = tactic_ref := f;
 
-fun tactic txt ctxt = METHOD (fn facts =>
- (ML_Context.use_mltext
-   ("let fun tactic (ctxt: Proof.context) (facts: thm list) : tactic =\n"
-     ^ txt ^ "\nin Method.set_tactic tactic end") false (SOME (Context.Proof ctxt));
-  ML_Context.setmp (SOME (Context.Proof ctxt)) (! tactic_ref ctxt) facts));
+fun ml_tactic txt ctxt facts =
+  (ML_Context.use_mltext
+    ("let fun tactic (ctxt: Proof.context) (facts: thm list) : tactic =\n"
+      ^ txt ^ "\nin Method.set_tactic tactic end") false (SOME (Context.Proof ctxt));
+    ML_Context.setmp (SOME (Context.Proof ctxt)) (! tactic_ref ctxt) facts);
+
+fun tactic txt ctxt = METHOD (ml_tactic txt ctxt);
+fun raw_tactic txt ctxt = RAW_METHOD (ml_tactic txt ctxt);
 
 
 
@@ -569,7 +572,8 @@
     "rename parameters of goal"),
   ("rotate_tac", goal_args (Scan.optional Args.int 1) Tactic.rotate_tac,
     "rotate assumptions of goal"),
-  ("tactic", simple_args Args.name tactic, "ML tactic as proof method")]);
+  ("tactic", simple_args Args.name tactic, "ML tactic as proof method"),
+  ("raw_tactic", simple_args Args.name raw_tactic, "ML tactic as raw proof method")]);
 
 
 (* outer parser *)