modernized structure Primitive_Defs;

--- a/src/HOL/Tools/record.ML	Mon Nov 02 20:34:59 2009 +0100
+++ b/src/HOL/Tools/record.ML	Mon Nov 02 20:38:46 2009 +0100
@@ -262,7 +262,7 @@
 infixr 0 ==>;
 
 val op $$ = Term.list_comb;
-val op :== = PrimitiveDefs.mk_defpair;
+val op :== = Primitive_Defs.mk_defpair;
 val op === = Trueprop o HOLogic.mk_eq;
 val op ==> = Logic.mk_implies;
 

--- a/src/HOL/Tools/typedef.ML	Mon Nov 02 20:34:59 2009 +0100
+++ b/src/HOL/Tools/typedef.ML	Mon Nov 02 20:38:46 2009 +0100
@@ -115,7 +115,7 @@
         theory
         |> Sign.add_consts_i [(name, setT', NoSyn)]
         |> PureThy.add_defs false [Thm.no_attributes (apfst (Binding.name)
-            (PrimitiveDefs.mk_defpair (setC, set)))]
+            (Primitive_Defs.mk_defpair (setC, set)))]
         |-> (fn [th] => pair (SOME th))
       else (NONE, theory);
     fun contract_def NONE th = th

--- a/src/Pure/Isar/local_defs.ML	Mon Nov 02 20:34:59 2009 +0100
+++ b/src/Pure/Isar/local_defs.ML	Mon Nov 02 20:38:46 2009 +0100
@@ -47,11 +47,11 @@
       quote (Syntax.string_of_term ctxt eq));
     val ((lhs, _), eq') = eq
       |> Sign.no_vars (Syntax.pp ctxt)
-      |> PrimitiveDefs.dest_def ctxt Term.is_Free (Variable.is_fixed ctxt) (K true)
+      |> Primitive_Defs.dest_def ctxt Term.is_Free (Variable.is_fixed ctxt) (K true)
       handle TERM (msg, _) => err msg | ERROR msg => err msg;
   in (Term.dest_Free (Term.head_of lhs), eq') end;
 
-val abs_def = PrimitiveDefs.abs_def #>> Term.dest_Free;
+val abs_def = Primitive_Defs.abs_def #>> Term.dest_Free;
 
 fun mk_def ctxt args =
   let

--- a/src/Pure/primitive_defs.ML	Mon Nov 02 20:34:59 2009 +0100
+++ b/src/Pure/primitive_defs.ML	Mon Nov 02 20:38:46 2009 +0100
@@ -12,7 +12,7 @@
   val mk_defpair: term * term -> string * term
 end;
 
-structure PrimitiveDefs: PRIMITIVE_DEFS =
+structure Primitive_Defs: PRIMITIVE_DEFS =
 struct
 
 fun term_kind (Const _) = "existing constant "

--- a/src/Pure/sign.ML	Mon Nov 02 20:34:59 2009 +0100
+++ b/src/Pure/sign.ML	Mon Nov 02 20:38:46 2009 +0100
@@ -392,7 +392,7 @@
   let val ((lhs, rhs), _) = tm
     |> no_vars (Syntax.pp ctxt)
     |> Logic.strip_imp_concl
-    |> PrimitiveDefs.dest_def ctxt Term.is_Const (K false) (K false)
+    |> Primitive_Defs.dest_def ctxt Term.is_Const (K false) (K false)
   in (Term.dest_Const (Term.head_of lhs), rhs) end
   handle TERM (msg, _) => error msg;
 

--- a/src/ZF/Tools/datatype_package.ML	Mon Nov 02 20:34:59 2009 +0100
+++ b/src/ZF/Tools/datatype_package.ML	Mon Nov 02 20:38:46 2009 +0100
@@ -108,7 +108,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*)
-            PrimitiveDefs.mk_defpair (list_comb (Const (full_name name, T), args),
+            Primitive_Defs.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;
@@ -157,7 +157,7 @@
   val case_const = Const (case_name, case_typ);
   val case_tm = list_comb (case_const, case_args);
 
-  val case_def = PrimitiveDefs.mk_defpair
+  val case_def = Primitive_Defs.mk_defpair
     (case_tm, Balanced_Tree.make (fn (t1, t2) => Su.elim $ t1 $ t2) (map call_case case_lists));
 
 
@@ -232,7 +232,7 @@
   val recursor_cases = map call_recursor (flat case_lists ~~ flat recursor_lists);
 
   val recursor_def =
-      PrimitiveDefs.mk_defpair
+      Primitive_Defs.mk_defpair
         (recursor_tm,
          @{const Univ.Vrecursor} $
            absfree ("rec", @{typ i}, list_comb (case_const, recursor_cases)));

--- a/src/ZF/Tools/inductive_package.ML	Mon Nov 02 20:34:59 2009 +0100
+++ b/src/ZF/Tools/inductive_package.ML	Mon Nov 02 20:38:46 2009 +0100
@@ -156,7 +156,7 @@
   val big_rec_tm = list_comb(Const(big_rec_name,recT), rec_params);
 
   (*The individual sets must already be declared*)
-  val axpairs = map PrimitiveDefs.mk_defpair
+  val axpairs = map Primitive_Defs.mk_defpair
         ((big_rec_tm, fp_rhs) ::
          (case parts of
              [_] => []                        (*no mutual recursion*)