--- a/src/HOL/Tools/split_rule.ML Thu Apr 07 09:24:35 2005 +0200
+++ b/src/HOL/Tools/split_rule.ML Thu Apr 07 09:25:33 2005 +0200
@@ -2,7 +2,7 @@
ID: $Id$
Author: Stefan Berghofer, David von Oheimb, and Markus Wenzel, TU Muenchen
-SOME tools for managing tupled arguments and abstractions in rules.
+Some tools for managing tupled arguments and abstractions in rules.
*)
signature BASIC_SPLIT_RULE =
@@ -130,6 +130,8 @@
(* attribute syntax *)
+(* FIXME dynamically scoped due to Args.name/pair_tac *)
+
fun split_format x = Attrib.syntax
(Scan.lift (Args.parens (Args.$$$ "complete"))
>> K (Drule.rule_attribute (K complete_split_rule)) ||