--- a/src/Pure/Isar/method.ML Wed Apr 09 17:54:09 2014 +0200
+++ b/src/Pure/Isar/method.ML Wed Apr 09 20:58:32 2014 +0200
@@ -513,9 +513,9 @@
setup @{binding rotate_tac} (Args.goal_spec -- Scan.lift (Scan.optional Parse.int 1) >>
(fn (quant, i) => K (SIMPLE_METHOD'' quant (rotate_tac i))))
"rotate assumptions of goal" #>
- setup @{binding tactic} (Scan.lift Args.name_source_position >> tactic)
+ setup @{binding tactic} (Scan.lift Args.text_source_position >> tactic)
"ML tactic as proof method" #>
- setup @{binding raw_tactic} (Scan.lift Args.name_source_position >> raw_tactic)
+ setup @{binding raw_tactic} (Scan.lift Args.text_source_position >> raw_tactic)
"ML tactic as raw proof method");