# HG changeset patch
# User wenzelm
# Date 1267134412 -3600
# Node ID 2fcd08c624958bb0546aba7f155477c76bf9fc2a
# Parent  b8c62d60195c131368e0ae8e12c212dcd0b15598
modernized structure Split_Rule;
tuned signature;
more antiquotations;

diff -r b8c62d60195c -r 2fcd08c62495 src/HOL/Product_Type.thy
--- a/src/HOL/Product_Type.thy	Thu Feb 25 22:32:09 2010 +0100
+++ b/src/HOL/Product_Type.thy	Thu Feb 25 22:46:52 2010 +0100
@@ -635,7 +635,7 @@
   by (simp only: internal_split_def split_conv)
 
 use "Tools/split_rule.ML"
-setup SplitRule.setup
+setup Split_Rule.setup
 
 hide const internal_split
 
diff -r b8c62d60195c -r 2fcd08c62495 src/HOL/Tools/TFL/post.ML
--- a/src/HOL/Tools/TFL/post.ML	Thu Feb 25 22:32:09 2010 +0100
+++ b/src/HOL/Tools/TFL/post.ML	Thu Feb 25 22:46:52 2010 +0100
@@ -125,7 +125,7 @@
 
 (*lcp: curry the predicate of the induction rule*)
 fun curry_rule rl =
-  SplitRule.split_rule_var (Term.head_of (HOLogic.dest_Trueprop (concl_of rl))) rl;
+  Split_Rule.split_rule_var (Term.head_of (HOLogic.dest_Trueprop (concl_of rl))) rl;
 
 (*lcp: put a theorem into Isabelle form, using meta-level connectives*)
 val meta_outer =
diff -r b8c62d60195c -r 2fcd08c62495 src/HOL/Tools/split_rule.ML
--- a/src/HOL/Tools/split_rule.ML	Thu Feb 25 22:32:09 2010 +0100
+++ b/src/HOL/Tools/split_rule.ML	Thu Feb 25 22:46:52 2010 +0100
@@ -4,49 +4,34 @@
 Some tools for managing tupled arguments and abstractions in rules.
 *)
 
-signature BASIC_SPLIT_RULE =
+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
-end;
-
-signature SPLIT_RULE =
-sig
-  include BASIC_SPLIT_RULE
-  val split_rule_var: term -> thm -> thm
-  val split_rule_goal: Proof.context -> string list list -> thm -> thm
   val setup: theory -> theory
 end;
 
-structure SplitRule: SPLIT_RULE =
+structure Split_Rule: SPLIT_RULE =
 struct
 
-
-
-(** theory context references **)
-
-val split_conv = thm "split_conv";
-val fst_conv = thm "fst_conv";
-val snd_conv = thm "snd_conv";
-
-fun internal_split_const (Ta, Tb, Tc) =
-  Const ("Product_Type.internal_split", [[Ta, Tb] ---> Tc, HOLogic.mk_prodT (Ta, Tb)] ---> Tc);
-
-val internal_split_def = thm "internal_split_def";
-val internal_split_conv = thm "internal_split_conv";
-
-
-
 (** split rules **)
 
-val eval_internal_split = hol_simplify [internal_split_def] o hol_simplify [internal_split_conv];
+fun internal_split_const (Ta, Tb, Tc) =
+  Const (@{const_name Product_Type.internal_split},
+    [[Ta, Tb] ---> Tc, HOLogic.mk_prodT (Ta, Tb)] ---> Tc);
+
+val eval_internal_split =
+  hol_simplify [@{thm internal_split_def}] o hol_simplify [@{thm internal_split_conv}];
+
 val remove_internal_split = eval_internal_split o split_all;
 
 
 (*In ap_split S T u, term u expects separate arguments for the factors of S,
   with result type T.  The call creates a new term expecting one argument
   of type S.*)
-fun ap_split (Type ("*", [T1, T2])) T3 u =
+fun ap_split (Type (@{type_name "*"}, [T1, T2])) T3 u =
       internal_split_const (T1, T2, T3) $
       Abs ("v", T1,
           ap_split T2 T3
@@ -127,7 +112,7 @@
   THEN' hyp_subst_tac
   THEN' K prune_params_tac;
 
-val split_rule_ss = HOL_basic_ss addsimps [split_conv, fst_conv, snd_conv];
+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
@@ -159,5 +144,3 @@
 
 end;
 
-structure BasicSplitRule: BASIC_SPLIT_RULE = SplitRule;
-open BasicSplitRule;