modernized structure Primitive_Defs;
authorwenzelm
Mon Nov 02 20:38:46 2009 +0100 (2009-11-02)
changeset 33385fb2358edcfb6
parent 33384 1b5ba4e6a953
child 33386 ff29d1549aca
modernized structure Primitive_Defs;
src/HOL/Tools/record.ML
src/HOL/Tools/typedef.ML
src/Pure/Isar/local_defs.ML
src/Pure/primitive_defs.ML
src/Pure/sign.ML
src/ZF/Tools/datatype_package.ML
src/ZF/Tools/inductive_package.ML
     1.1 --- a/src/HOL/Tools/record.ML	Mon Nov 02 20:34:59 2009 +0100
     1.2 +++ b/src/HOL/Tools/record.ML	Mon Nov 02 20:38:46 2009 +0100
     1.3 @@ -262,7 +262,7 @@
     1.4  infixr 0 ==>;
     1.5  
     1.6  val op $$ = Term.list_comb;
     1.7 -val op :== = PrimitiveDefs.mk_defpair;
     1.8 +val op :== = Primitive_Defs.mk_defpair;
     1.9  val op === = Trueprop o HOLogic.mk_eq;
    1.10  val op ==> = Logic.mk_implies;
    1.11  
     2.1 --- a/src/HOL/Tools/typedef.ML	Mon Nov 02 20:34:59 2009 +0100
     2.2 +++ b/src/HOL/Tools/typedef.ML	Mon Nov 02 20:38:46 2009 +0100
     2.3 @@ -115,7 +115,7 @@
     2.4          theory
     2.5          |> Sign.add_consts_i [(name, setT', NoSyn)]
     2.6          |> PureThy.add_defs false [Thm.no_attributes (apfst (Binding.name)
     2.7 -            (PrimitiveDefs.mk_defpair (setC, set)))]
     2.8 +            (Primitive_Defs.mk_defpair (setC, set)))]
     2.9          |-> (fn [th] => pair (SOME th))
    2.10        else (NONE, theory);
    2.11      fun contract_def NONE th = th
     3.1 --- a/src/Pure/Isar/local_defs.ML	Mon Nov 02 20:34:59 2009 +0100
     3.2 +++ b/src/Pure/Isar/local_defs.ML	Mon Nov 02 20:38:46 2009 +0100
     3.3 @@ -47,11 +47,11 @@
     3.4        quote (Syntax.string_of_term ctxt eq));
     3.5      val ((lhs, _), eq') = eq
     3.6        |> Sign.no_vars (Syntax.pp ctxt)
     3.7 -      |> PrimitiveDefs.dest_def ctxt Term.is_Free (Variable.is_fixed ctxt) (K true)
     3.8 +      |> Primitive_Defs.dest_def ctxt Term.is_Free (Variable.is_fixed ctxt) (K true)
     3.9        handle TERM (msg, _) => err msg | ERROR msg => err msg;
    3.10    in (Term.dest_Free (Term.head_of lhs), eq') end;
    3.11  
    3.12 -val abs_def = PrimitiveDefs.abs_def #>> Term.dest_Free;
    3.13 +val abs_def = Primitive_Defs.abs_def #>> Term.dest_Free;
    3.14  
    3.15  fun mk_def ctxt args =
    3.16    let
     4.1 --- a/src/Pure/primitive_defs.ML	Mon Nov 02 20:34:59 2009 +0100
     4.2 +++ b/src/Pure/primitive_defs.ML	Mon Nov 02 20:38:46 2009 +0100
     4.3 @@ -12,7 +12,7 @@
     4.4    val mk_defpair: term * term -> string * term
     4.5  end;
     4.6  
     4.7 -structure PrimitiveDefs: PRIMITIVE_DEFS =
     4.8 +structure Primitive_Defs: PRIMITIVE_DEFS =
     4.9  struct
    4.10  
    4.11  fun term_kind (Const _) = "existing constant "
     5.1 --- a/src/Pure/sign.ML	Mon Nov 02 20:34:59 2009 +0100
     5.2 +++ b/src/Pure/sign.ML	Mon Nov 02 20:38:46 2009 +0100
     5.3 @@ -392,7 +392,7 @@
     5.4    let val ((lhs, rhs), _) = tm
     5.5      |> no_vars (Syntax.pp ctxt)
     5.6      |> Logic.strip_imp_concl
     5.7 -    |> PrimitiveDefs.dest_def ctxt Term.is_Const (K false) (K false)
     5.8 +    |> Primitive_Defs.dest_def ctxt Term.is_Const (K false) (K false)
     5.9    in (Term.dest_Const (Term.head_of lhs), rhs) end
    5.10    handle TERM (msg, _) => error msg;
    5.11  
     6.1 --- a/src/ZF/Tools/datatype_package.ML	Mon Nov 02 20:34:59 2009 +0100
     6.2 +++ b/src/ZF/Tools/datatype_package.ML	Mon Nov 02 20:38:46 2009 +0100
     6.3 @@ -108,7 +108,7 @@
     6.4      let val ncon = length con_ty_list    (*number of constructors*)
     6.5          fun mk_def (((id,T,syn), name, args, prems), kcon) =
     6.6                (*kcon is index of constructor*)
     6.7 -            PrimitiveDefs.mk_defpair (list_comb (Const (full_name name, T), args),
     6.8 +            Primitive_Defs.mk_defpair (list_comb (Const (full_name name, T), args),
     6.9                          mk_inject npart kpart
    6.10                          (mk_inject ncon kcon (mk_tuple args)))
    6.11      in  ListPair.map mk_def (con_ty_list, 1 upto ncon)  end;
    6.12 @@ -157,7 +157,7 @@
    6.13    val case_const = Const (case_name, case_typ);
    6.14    val case_tm = list_comb (case_const, case_args);
    6.15  
    6.16 -  val case_def = PrimitiveDefs.mk_defpair
    6.17 +  val case_def = Primitive_Defs.mk_defpair
    6.18      (case_tm, Balanced_Tree.make (fn (t1, t2) => Su.elim $ t1 $ t2) (map call_case case_lists));
    6.19  
    6.20  
    6.21 @@ -232,7 +232,7 @@
    6.22    val recursor_cases = map call_recursor (flat case_lists ~~ flat recursor_lists);
    6.23  
    6.24    val recursor_def =
    6.25 -      PrimitiveDefs.mk_defpair
    6.26 +      Primitive_Defs.mk_defpair
    6.27          (recursor_tm,
    6.28           @{const Univ.Vrecursor} $
    6.29             absfree ("rec", @{typ i}, list_comb (case_const, recursor_cases)));
     7.1 --- a/src/ZF/Tools/inductive_package.ML	Mon Nov 02 20:34:59 2009 +0100
     7.2 +++ b/src/ZF/Tools/inductive_package.ML	Mon Nov 02 20:38:46 2009 +0100
     7.3 @@ -156,7 +156,7 @@
     7.4    val big_rec_tm = list_comb(Const(big_rec_name,recT), rec_params);
     7.5  
     7.6    (*The individual sets must already be declared*)
     7.7 -  val axpairs = map PrimitiveDefs.mk_defpair
     7.8 +  val axpairs = map Primitive_Defs.mk_defpair
     7.9          ((big_rec_tm, fp_rhs) ::
    7.10           (case parts of
    7.11               [_] => []                        (*no mutual recursion*)