# HG changeset patch
# User krauss
# Date 1288998632 -3600
# Node ID cb9fd7dd641c793c9cb9de8bfa09e07fa95b8e0f
# Parent  e4c9e0dad473dc2671ab43fda04ead39fb48388f
abolished obscure goal variant of [split_format] -- unused (cf. d1c14898fd04), unrelated to '(complete)' variant, and not at all canonical

diff -r e4c9e0dad473 -r cb9fd7dd641c NEWS
--- a/NEWS	Fri Nov 05 23:19:20 2010 +0100
+++ b/NEWS	Sat Nov 06 00:10:32 2010 +0100
@@ -354,6 +354,9 @@
     yices_options
     smt_datatypes
 
+* Removed [split_format ... and ... and ...] version of
+[split_format].  Potential INCOMPATIBILITY.
+
 *** FOL ***
 
 * All constant names are now qualified.  INCOMPATIBILITY.
diff -r e4c9e0dad473 -r cb9fd7dd641c doc-src/IsarRef/Thy/HOL_Specific.thy
--- a/doc-src/IsarRef/Thy/HOL_Specific.thy	Fri Nov 05 23:19:20 2010 +0100
+++ b/doc-src/IsarRef/Thy/HOL_Specific.thy	Sat Nov 06 00:10:32 2010 +0100
@@ -72,22 +72,18 @@
   \end{matharray}
 
   \begin{rail}
-    'split_format' ((( name * ) + 'and') | ('(' 'complete' ')'))
+    'split_format' '(' 'complete' ')'
     ;
   \end{rail}
 
   \begin{description}
   
-  \item @{attribute (HOL) split_format}~@{text "p\<^sub>1 \<dots> p\<^sub>m \<AND> \<dots>
-  \<AND> q\<^sub>1 \<dots> q\<^sub>n"} puts expressions of low-level tuple types into
-  canonical form as specified by the arguments given; the @{text i}-th
-  collection of arguments refers to occurrences in premise @{text i}
-  of the rule.  The ``@{text "(complete)"}'' option causes \emph{all}
+  \item @{attribute (HOL) split_format}\ @{text "(complete)"} causes
   arguments in function applications to be represented canonically
   according to their tuple type structure.
 
-  Note that these operations tend to invent funny names for new local
-  parameters to be introduced.
+  Note that this operation tends to invent funny names for new local
+  parameters introduced.
 
   \end{description}
 *}
diff -r e4c9e0dad473 -r cb9fd7dd641c doc-src/IsarRef/Thy/document/HOL_Specific.tex
--- a/doc-src/IsarRef/Thy/document/HOL_Specific.tex	Fri Nov 05 23:19:20 2010 +0100
+++ b/doc-src/IsarRef/Thy/document/HOL_Specific.tex	Sat Nov 06 00:10:32 2010 +0100
@@ -93,21 +93,18 @@
   \end{matharray}
 
   \begin{rail}
-    'split_format' ((( name * ) + 'and') | ('(' 'complete' ')'))
+    'split_format' '(' 'complete' ')'
     ;
   \end{rail}
 
   \begin{description}
   
-  \item \hyperlink{attribute.HOL.split-format}{\mbox{\isa{split{\isacharunderscore}format}}}~\isa{{\isachardoublequote}p\isactrlsub {\isadigit{1}}\ {\isasymdots}\ p\isactrlsub m\ {\isasymAND}\ {\isasymdots}\ {\isasymAND}\ q\isactrlsub {\isadigit{1}}\ {\isasymdots}\ q\isactrlsub n{\isachardoublequote}} puts expressions of low-level tuple types into
-  canonical form as specified by the arguments given; the \isa{i}-th
-  collection of arguments refers to occurrences in premise \isa{i}
-  of the rule.  The ``\isa{{\isachardoublequote}{\isacharparenleft}complete{\isacharparenright}{\isachardoublequote}}'' option causes \emph{all}
+  \item \hyperlink{attribute.HOL.split-format}{\mbox{\isa{split{\isacharunderscore}format}}}\ \isa{{\isachardoublequote}{\isacharparenleft}complete{\isacharparenright}{\isachardoublequote}} causes
   arguments in function applications to be represented canonically
   according to their tuple type structure.
 
-  Note that these operations tend to invent funny names for new local
-  parameters to be introduced.
+  Note that this operation tends to invent funny names for new local
+  parameters introduced.
 
   \end{description}%
 \end{isamarkuptext}%
diff -r e4c9e0dad473 -r cb9fd7dd641c src/HOL/Tools/split_rule.ML
--- a/src/HOL/Tools/split_rule.ML	Fri Nov 05 23:19:20 2010 +0100
+++ b/src/HOL/Tools/split_rule.ML	Sat Nov 06 00:10:32 2010 +0100
@@ -7,7 +7,6 @@
 signature SPLIT_RULE =
 sig
   val split_rule_var: term -> thm -> thm
-  val split_rule_goal: Proof.context -> string list list -> thm -> thm
   val split_rule: thm -> thm
   val complete_split_rule: thm -> thm
   val setup: theory -> theory
@@ -48,7 +47,7 @@
   | split_rule_var' t rl = rl;
 
 
-(* complete splitting of partially splitted rules *)
+(* complete splitting of partially split rules *)
 
 fun ap_split' (T::Ts) U u = Abs ("v", T, ap_split' Ts U
       (ap_split T (maps HOLogic.flatten_tupleT Ts ---> U)
@@ -107,37 +106,12 @@
   end;
 
 
-fun pair_tac ctxt s =
-  res_inst_tac ctxt [(("y", 0), s)] @{thm prod.exhaust}
-  THEN' hyp_subst_tac
-  THEN' K prune_params_tac;
-
-val split_rule_ss = HOL_basic_ss addsimps [@{thm split_conv}, @{thm fst_conv}, @{thm snd_conv}];
-
-fun split_rule_goal ctxt xss rl =
-  let
-    fun one_split i s = Tactic.rule_by_tactic ctxt (pair_tac ctxt s i);
-    fun one_goal (i, xs) = fold (one_split (i + 1)) xs;
-  in
-    rl
-    |> fold_index one_goal xss
-    |> Simplifier.full_simplify split_rule_ss
-    |> Drule.export_without_context
-    |> Rule_Cases.save rl
-  end;
-
-
 (* attribute syntax *)
 
-(* FIXME dynamically scoped due to Args.name_source/pair_tac *)
-
 val setup =
   Attrib.setup @{binding split_format}
     (Scan.lift
-     (Args.parens (Args.$$$ "complete") >> K (Thm.rule_attribute (K complete_split_rule)) ||
-      Parse.and_list1 (Scan.repeat Args.name_source)
-        >> (fn xss => Thm.rule_attribute (fn context =>
-            split_rule_goal (Context.proof_of context) xss))))
+     (Args.parens (Args.$$$ "complete") >> K (Thm.rule_attribute (K complete_split_rule))))
     "split pair-typed subterms in premises, or function arguments" #>
   Attrib.setup @{binding split_rule} (Scan.succeed (Thm.rule_attribute (K split_rule)))
     "curries ALL function variables occurring in a rule's conclusion";