# HG changeset patch
# User wenzelm
# Date 1187090412 -7200
# Node ID d86dbde1000c2be6bef5d8330b6db958a1980f67
# Parent  5180e11e4e4242a0208fe898d3c07a92a3f9208e
PrimitiveDefs.mk_defpair;

diff -r 5180e11e4e42 -r d86dbde1000c src/HOL/Tools/record_package.ML
--- a/src/HOL/Tools/record_package.ML	Tue Aug 14 00:52:59 2007 +0200
+++ b/src/HOL/Tools/record_package.ML	Tue Aug 14 13:20:12 2007 +0200
@@ -137,7 +137,7 @@
 infixr 0 ==>;
 
 val (op $$) = Term.list_comb;
-val (op :==) = Logic.mk_defpair;
+val (op :==) = PrimitiveDefs.mk_defpair;
 val (op ===) = Trueprop o HOLogic.mk_eq;
 val (op ==>) = Logic.mk_implies;
 
diff -r 5180e11e4e42 -r d86dbde1000c src/HOL/Tools/typedef_package.ML
--- a/src/HOL/Tools/typedef_package.ML	Tue Aug 14 00:52:59 2007 +0200
+++ b/src/HOL/Tools/typedef_package.ML	Tue Aug 14 13:20:12 2007 +0200
@@ -155,7 +155,7 @@
        ((if def then [(name, setT', NoSyn)] else []) @
         [(Rep_name, newT --> oldT, NoSyn),
          (Abs_name, oldT --> newT, NoSyn)])
-      #> add_def (Logic.mk_defpair (setC, set))
+      #> add_def (PrimitiveDefs.mk_defpair (setC, set))
       ##>> PureThy.add_axioms_i [((typedef_name, typedef_prop),
           [apsnd (fn cond_axm => nonempty RS cond_axm)])]
       ##> Theory.add_deps "" (dest_Const RepC) typedef_deps
diff -r 5180e11e4e42 -r d86dbde1000c src/ZF/Tools/datatype_package.ML
--- a/src/ZF/Tools/datatype_package.ML	Tue Aug 14 00:52:59 2007 +0200
+++ b/src/ZF/Tools/datatype_package.ML	Tue Aug 14 13:20:12 2007 +0200
@@ -92,7 +92,7 @@
     let val ncon = length con_ty_list    (*number of constructors*)
         fun mk_def (((id,T,syn), name, args, prems), kcon) =
               (*kcon is index of constructor*)
-            Logic.mk_defpair (list_comb (Const (full_name name, T), args),
+            PrimitiveDefs.mk_defpair (list_comb (Const (full_name name, T), args),
                         mk_inject npart kpart
                         (mk_inject ncon kcon (mk_tuple args)))
     in  ListPair.map mk_def (con_ty_list, 1 upto ncon)  end;
@@ -141,7 +141,7 @@
   val case_const = Const (case_name, case_typ);
   val case_tm = list_comb (case_const, case_args);
 
-  val case_def = Logic.mk_defpair
+  val case_def = PrimitiveDefs.mk_defpair
     (case_tm, BalancedTree.make (fn (t1, t2) => Su.elim $ t1 $ t2) (map call_case case_lists));
 
 
@@ -218,7 +218,7 @@
                          (List.concat case_lists ~~ List.concat recursor_lists)
 
   val recursor_def =
-      Logic.mk_defpair
+      PrimitiveDefs.mk_defpair
         (recursor_tm,
          Ind_Syntax.Vrecursor_const $
            absfree ("rec", iT, list_comb (case_const, recursor_cases)));
diff -r 5180e11e4e42 -r d86dbde1000c src/ZF/Tools/inductive_package.ML
--- a/src/ZF/Tools/inductive_package.ML	Tue Aug 14 00:52:59 2007 +0200
+++ b/src/ZF/Tools/inductive_package.ML	Tue Aug 14 13:20:12 2007 +0200
@@ -157,7 +157,7 @@
   val big_rec_tm = list_comb(Const(big_rec_name,recT), rec_params);
 
   (*The individual sets must already be declared*)
-  val axpairs = map Logic.mk_defpair
+  val axpairs = map PrimitiveDefs.mk_defpair
         ((big_rec_tm, fp_rhs) ::
          (case parts of
              [_] => []                        (*no mutual recursion*)