1.1 --- a/NEWS	Fri Nov 05 23:19:20 2010 +0100
     1.2 +++ b/NEWS	Sat Nov 06 00:10:32 2010 +0100
     1.3 @@ -354,6 +354,9 @@
     1.4      yices_options
     1.5      smt_datatypes
     1.6  
     1.7 +* Removed [split_format ... and ... and ...] version of
     1.8 +[split_format].  Potential INCOMPATIBILITY.
     1.9 +
    1.10  *** FOL ***
    1.11  
    1.12  * All constant names are now qualified.  INCOMPATIBILITY.

     2.1 --- a/doc-src/IsarRef/Thy/HOL_Specific.thy	Fri Nov 05 23:19:20 2010 +0100
     2.2 +++ b/doc-src/IsarRef/Thy/HOL_Specific.thy	Sat Nov 06 00:10:32 2010 +0100
     2.3 @@ -72,22 +72,18 @@
     2.4    \end{matharray}
     2.5  
     2.6    \begin{rail}
     2.7 -    'split_format' ((( name * ) + 'and') | ('(' 'complete' ')'))
     2.8 +    'split_format' '(' 'complete' ')'
     2.9      ;
    2.10    \end{rail}
    2.11  
    2.12    \begin{description}
    2.13    
    2.14 -  \item @{attribute (HOL) split_format}~@{text "p\<^sub>1 \<dots> p\<^sub>m \<AND> \<dots>
    2.15 -  \<AND> q\<^sub>1 \<dots> q\<^sub>n"} puts expressions of low-level tuple types into
    2.16 -  canonical form as specified by the arguments given; the @{text i}-th
    2.17 -  collection of arguments refers to occurrences in premise @{text i}
    2.18 -  of the rule.  The ``@{text "(complete)"}'' option causes \emph{all}
    2.19 +  \item @{attribute (HOL) split_format}\ @{text "(complete)"} causes
    2.20    arguments in function applications to be represented canonically
    2.21    according to their tuple type structure.
    2.22  
    2.23 -  Note that these operations tend to invent funny names for new local
    2.24 -  parameters to be introduced.
    2.25 +  Note that this operation tends to invent funny names for new local
    2.26 +  parameters introduced.
    2.27  
    2.28    \end{description}
    2.29  *}

     3.1 --- a/doc-src/IsarRef/Thy/document/HOL_Specific.tex	Fri Nov 05 23:19:20 2010 +0100
     3.2 +++ b/doc-src/IsarRef/Thy/document/HOL_Specific.tex	Sat Nov 06 00:10:32 2010 +0100
     3.3 @@ -93,21 +93,18 @@
     3.4    \end{matharray}
     3.5  
     3.6    \begin{rail}
     3.7 -    'split_format' ((( name * ) + 'and') | ('(' 'complete' ')'))
     3.8 +    'split_format' '(' 'complete' ')'
     3.9      ;
    3.10    \end{rail}
    3.11  
    3.12    \begin{description}
    3.13    
    3.14 -  \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
    3.15 -  canonical form as specified by the arguments given; the \isa{i}-th
    3.16 -  collection of arguments refers to occurrences in premise \isa{i}
    3.17 -  of the rule.  The ``\isa{{\isachardoublequote}{\isacharparenleft}complete{\isacharparenright}{\isachardoublequote}}'' option causes \emph{all}
    3.18 +  \item \hyperlink{attribute.HOL.split-format}{\mbox{\isa{split{\isacharunderscore}format}}}\ \isa{{\isachardoublequote}{\isacharparenleft}complete{\isacharparenright}{\isachardoublequote}} causes
    3.19    arguments in function applications to be represented canonically
    3.20    according to their tuple type structure.
    3.21  
    3.22 -  Note that these operations tend to invent funny names for new local
    3.23 -  parameters to be introduced.
    3.24 +  Note that this operation tends to invent funny names for new local
    3.25 +  parameters introduced.
    3.26  
    3.27    \end{description}%
    3.28  \end{isamarkuptext}%

     4.1 --- a/src/HOL/Tools/split_rule.ML	Fri Nov 05 23:19:20 2010 +0100
     4.2 +++ b/src/HOL/Tools/split_rule.ML	Sat Nov 06 00:10:32 2010 +0100
     4.3 @@ -7,7 +7,6 @@
     4.4  signature SPLIT_RULE =
     4.5  sig
     4.6    val split_rule_var: term -> thm -> thm
     4.7 -  val split_rule_goal: Proof.context -> string list list -> thm -> thm
     4.8    val split_rule: thm -> thm
     4.9    val complete_split_rule: thm -> thm
    4.10    val setup: theory -> theory
    4.11 @@ -48,7 +47,7 @@
    4.12    | split_rule_var' t rl = rl;
    4.13  
    4.14  
    4.15 -(* complete splitting of partially splitted rules *)
    4.16 +(* complete splitting of partially split rules *)
    4.17  
    4.18  fun ap_split' (T::Ts) U u = Abs ("v", T, ap_split' Ts U
    4.19        (ap_split T (maps HOLogic.flatten_tupleT Ts ---> U)
    4.20 @@ -107,37 +106,12 @@
    4.21    end;
    4.22  
    4.23  
    4.24 -fun pair_tac ctxt s =
    4.25 -  res_inst_tac ctxt [(("y", 0), s)] @{thm prod.exhaust}
    4.26 -  THEN' hyp_subst_tac
    4.27 -  THEN' K prune_params_tac;
    4.28 -
    4.29 -val split_rule_ss = HOL_basic_ss addsimps [@{thm split_conv}, @{thm fst_conv}, @{thm snd_conv}];
    4.30 -
    4.31 -fun split_rule_goal ctxt xss rl =
    4.32 -  let
    4.33 -    fun one_split i s = Tactic.rule_by_tactic ctxt (pair_tac ctxt s i);
    4.34 -    fun one_goal (i, xs) = fold (one_split (i + 1)) xs;
    4.35 -  in
    4.36 -    rl
    4.37 -    |> fold_index one_goal xss
    4.38 -    |> Simplifier.full_simplify split_rule_ss
    4.39 -    |> Drule.export_without_context
    4.40 -    |> Rule_Cases.save rl
    4.41 -  end;
    4.42 -
    4.43 -
    4.44  (* attribute syntax *)
    4.45  
    4.46 -(* FIXME dynamically scoped due to Args.name_source/pair_tac *)
    4.47 -
    4.48  val setup =
    4.49    Attrib.setup @{binding split_format}
    4.50      (Scan.lift
    4.51 -     (Args.parens (Args.$$$ "complete") >> K (Thm.rule_attribute (K complete_split_rule)) ||
    4.52 -      Parse.and_list1 (Scan.repeat Args.name_source)
    4.53 -        >> (fn xss => Thm.rule_attribute (fn context =>
    4.54 -            split_rule_goal (Context.proof_of context) xss))))
    4.55 +     (Args.parens (Args.$$$ "complete") >> K (Thm.rule_attribute (K complete_split_rule))))
    4.56      "split pair-typed subterms in premises, or function arguments" #>
    4.57    Attrib.setup @{binding split_rule} (Scan.succeed (Thm.rule_attribute (K split_rule)))
    4.58      "curries ALL function variables occurring in a rule's conclusion";