renamed LocalTheory.def to LocalTheory.define;
authorwenzelm
Sat Oct 13 17:16:39 2007 +0200 (2007-10-13)
changeset 250162bcac52d7abc
parent 25015 1a84a9ae9d58
child 25017 e82ab4962f80
renamed LocalTheory.def to LocalTheory.define;
src/HOL/Tools/function_package/fundef_core.ML
src/HOL/Tools/function_package/mutual.ML
src/HOL/Tools/inductive_package.ML
src/HOL/Tools/inductive_set_package.ML
src/Pure/Isar/instance.ML
src/Pure/Isar/specification.ML
     1.1 --- a/src/HOL/Tools/function_package/fundef_core.ML	Fri Oct 12 22:01:56 2007 +0200
     1.2 +++ b/src/HOL/Tools/function_package/fundef_core.ML	Sat Oct 13 17:16:39 2007 +0200
     1.3 @@ -482,7 +482,7 @@
     1.4                |> Syntax.check_term lthy
     1.5  
     1.6        val ((f, (_, f_defthm)), lthy) =
     1.7 -        LocalTheory.def Thm.internalK ((function_name fname, mixfix), ((fdefname, []), f_def)) lthy
     1.8 +        LocalTheory.define Thm.internalK ((function_name fname, mixfix), ((fdefname, []), f_def)) lthy
     1.9      in
    1.10        ((f, f_defthm), lthy)
    1.11      end
     2.1 --- a/src/HOL/Tools/function_package/mutual.ML	Fri Oct 12 22:01:56 2007 +0200
     2.2 +++ b/src/HOL/Tools/function_package/mutual.ML	Sat Oct 13 17:16:39 2007 +0200
     2.3 @@ -184,7 +184,7 @@
     2.4        fun def ((MutualPart {i=i, i'=i', fvar=(fname, fT), cargTs, f_def, ...}), (_, mixfix)) lthy =
     2.5            let
     2.6              val ((f, (_, f_defthm)), lthy') =
     2.7 -              LocalTheory.def Thm.internalK ((fname, mixfix),
     2.8 +              LocalTheory.define Thm.internalK ((fname, mixfix),
     2.9                                              ((fname ^ "_def", []), Term.subst_bound (fsum, f_def)))
    2.10                                lthy
    2.11            in
     3.1 --- a/src/HOL/Tools/inductive_package.ML	Fri Oct 12 22:01:56 2007 +0200
     3.2 +++ b/src/HOL/Tools/inductive_package.ML	Sat Oct 13 17:16:39 2007 +0200
     3.3 @@ -645,7 +645,7 @@
     3.4        space_implode "_" (map fst cnames_syn) else alt_name;
     3.5  
     3.6      val ((rec_const, (_, fp_def)), ctxt') = ctxt |>
     3.7 -      LocalTheory.def Thm.internalK
     3.8 +      LocalTheory.define Thm.internalK
     3.9          ((rec_name, case cnames_syn of [(_, syn)] => syn | _ => NoSyn),
    3.10           (("", []), fold_rev lambda params
    3.11             (Const (fp_name, (predT --> predT) --> predT) $ fp_fun)));
    3.12 @@ -662,7 +662,7 @@
    3.13              (list_comb (rec_const, params @ make_bool_args' bs i @
    3.14                make_args argTs (xs ~~ Ts)))))
    3.15          end) (cnames_syn ~~ cs);
    3.16 -    val (consts_defs, ctxt'') = fold_map (LocalTheory.def Thm.internalK) specs ctxt';
    3.17 +    val (consts_defs, ctxt'') = fold_map (LocalTheory.define Thm.internalK) specs ctxt';
    3.18      val preds = (case cs of [_] => [rec_const] | _ => map #1 consts_defs);
    3.19  
    3.20      val mono = prove_mono predT fp_fun monos ctxt''
     4.1 --- a/src/HOL/Tools/inductive_set_package.ML	Fri Oct 12 22:01:56 2007 +0200
     4.2 +++ b/src/HOL/Tools/inductive_set_package.ML	Sat Oct 13 17:16:39 2007 +0200
     4.3 @@ -468,7 +468,7 @@
     4.4          cs' intros' monos' params1 cnames_syn' ctxt;
     4.5  
     4.6      (* define inductive sets using previously defined predicates *)
     4.7 -    val (defs, ctxt2) = fold_map (LocalTheory.def Thm.internalK)
     4.8 +    val (defs, ctxt2) = fold_map (LocalTheory.define Thm.internalK)
     4.9        (map (fn ((c_syn, (fs, U, _)), p) => (c_syn, (("", []),
    4.10           fold_rev lambda params (HOLogic.Collect_const U $
    4.11             HOLogic.ap_split' fs U HOLogic.boolT (list_comb (p, params3))))))
     5.1 --- a/src/Pure/Isar/instance.ML	Fri Oct 12 22:01:56 2007 +0200
     5.2 +++ b/src/Pure/Isar/instance.ML	Sat Oct 13 17:16:39 2007 +0200
     5.3 @@ -49,7 +49,7 @@
     5.4          pretty = LocalTheory.pretty,
     5.5          axioms = LocalTheory.axioms,
     5.6          abbrev = LocalTheory.abbrev,
     5.7 -        def = LocalTheory.def,
     5.8 +        define = LocalTheory.define,
     5.9          notes = LocalTheory.notes,
    5.10          type_syntax = LocalTheory.type_syntax,
    5.11          term_syntax = LocalTheory.term_syntax,
     6.1 --- a/src/Pure/Isar/specification.ML	Fri Oct 12 22:01:56 2007 +0200
     6.2 +++ b/src/Pure/Isar/specification.ML	Sat Oct 13 17:16:39 2007 +0200
     6.3 @@ -165,7 +165,7 @@
     6.4        if x = x' then mx
     6.5        else error ("Head of definition " ^ quote x ^ " differs from declaration " ^ quote x'));
     6.6      val ((lhs, (_, th)), lthy2) = lthy
     6.7 -      |> LocalTheory.def Thm.definitionK ((x, mx), ((name ^ "_raw", []), rhs));
     6.8 +      |> LocalTheory.define Thm.definitionK ((x, mx), ((name ^ "_raw", []), rhs));
     6.9      val ((b, [th']), lthy3) = lthy2
    6.10        |> LocalTheory.note Thm.definitionK
    6.11            ((name, Code.add_default_func_attr :: atts), [prove lthy2 th]);