# HG changeset patch
# User wenzelm
# Date 960316330 -7200
# Node ID 249c135057d773c680e1effb86fed0895ed4eb3a
# Parent  20ff649a0fd1858801d08985da156723ef0079cc
pair split: proper names of params;

diff -r 20ff649a0fd1 -r 249c135057d7 src/HOL/Tools/record_package.ML
--- a/src/HOL/Tools/record_package.ML	Tue Jun 06 20:31:43 2000 +0200
+++ b/src/HOL/Tools/record_package.ML	Tue Jun 06 20:32:10 2000 +0200
@@ -551,7 +551,7 @@
 
 (* field_definitions *)
 
-fun field_definitions fields names zeta moreT more vars named_vars thy =
+fun field_definitions fields names xs zeta moreT more vars named_vars thy =
   let
     val sign = Theory.sign_of thy;
     val base = Sign.base_name;
@@ -632,8 +632,8 @@
     val surj_pairs = map (prove [DatatypePackage.induct_tac "p" 1]
       (map Thm.symmetric field_defs @ dest_convs)) surj_props;
 
-    fun mk_split th = SplitPairedAll.rule (th RS eq_reflection);
-    val field_splits = map mk_split surj_pairs;
+    fun mk_split (x, th) = SplitPairedAll.rule_params x moreN (th RS eq_reflection);
+    val field_splits = map2 mk_split (xs, surj_pairs);
 
     val thms_thy =
       defs_thy
@@ -773,7 +773,7 @@
     val (fields_thy, field_simps, field_injects, field_splits) =
       thy
       |> Theory.add_path bname
-      |> field_definitions fields names zeta moreT more vars named_vars;
+      |> field_definitions fields names xs zeta moreT more vars named_vars;
 
     val named_splits = map2 (fn (c, th) => (suffix field_typeN c, th)) (names, field_splits);