# HG changeset patch
# User wenzelm
# Date 1243680777 -7200
# Node ID 0c5baf034d0e499e32e08393a769518c9f367140
# Parent  5e6b2b23701a026e4bb553146aa97fe982ff52bf
modernized method setup;

diff -r 5e6b2b23701a -r 0c5baf034d0e src/FOL/IFOL.thy
--- a/src/FOL/IFOL.thy	Sat May 30 11:57:36 2009 +0200
+++ b/src/FOL/IFOL.thy	Sat May 30 12:52:57 2009 +0200
@@ -610,7 +610,7 @@
 
 subsection {* Intuitionistic Reasoning *}
 
-setup {* Intuitionistic.method_setup "iprover" *}
+setup {* Intuitionistic.method_setup @{binding iprover} *}
 
 lemma impE':
   assumes 1: "P --> Q"
diff -r 5e6b2b23701a -r 0c5baf034d0e src/HOL/HOL.thy
--- a/src/HOL/HOL.thy	Sat May 30 11:57:36 2009 +0200
+++ b/src/HOL/HOL.thy	Sat May 30 12:52:57 2009 +0200
@@ -31,7 +31,7 @@
   ("Tools/recfun_codegen.ML")
 begin
 
-setup {* Intuitionistic.method_setup "iprover" *}
+setup {* Intuitionistic.method_setup @{binding iprover} *}
 
 
 subsection {* Primitive logic *}
diff -r 5e6b2b23701a -r 0c5baf034d0e src/Tools/intuitionistic.ML
--- a/src/Tools/intuitionistic.ML	Sat May 30 11:57:36 2009 +0200
+++ b/src/Tools/intuitionistic.ML	Sat May 30 12:52:57 2009 +0200
@@ -7,7 +7,7 @@
 signature INTUITIONISTIC =
 sig
   val prover_tac: Proof.context -> int option -> int -> tactic
-  val method_setup: bstring -> theory -> theory
+  val method_setup: binding -> theory -> theory
 end;
 
 structure Intuitionistic: INTUITIONISTIC =
@@ -84,15 +84,16 @@
   modifier introN Args.colon (Scan.succeed ()) ContextRules.intro,
   Args.del -- Args.colon >> K (I, ContextRules.rule_del)];
 
-val method =
-  Method.bang_sectioned_args' modifiers (Scan.lift (Scan.option OuterParse.nat))
-    (fn n => fn prems => fn ctxt => METHOD (fn facts =>
-      HEADGOAL (Method.insert_tac (prems @ facts) THEN'
-      ObjectLogic.atomize_prems_tac THEN' prover_tac ctxt n)));
-
 in
 
-fun method_setup name = Method.add_method (name, method, "intuitionistic proof search");
+fun method_setup name =
+  Method.setup name
+    (Args.bang_facts -- Scan.lift (Scan.option OuterParse.nat) --|
+      Method.sections modifiers >>
+      (fn (prems, n) => fn ctxt => METHOD (fn facts =>
+        HEADGOAL (Method.insert_tac (prems @ facts) THEN'
+        ObjectLogic.atomize_prems_tac THEN' prover_tac ctxt n))))
+    "intuitionistic proof search";
 
 end;