# HG changeset patch
# User wenzelm
# Date 1192288599 -7200
# Node ID 2bcac52d7abc796db3c1c28988de7e07e4a5585f
# Parent  1a84a9ae9d58715118a6cca733523417575f76e3
renamed LocalTheory.def to LocalTheory.define;

diff -r 1a84a9ae9d58 -r 2bcac52d7abc src/HOL/Tools/function_package/fundef_core.ML
--- a/src/HOL/Tools/function_package/fundef_core.ML	Fri Oct 12 22:01:56 2007 +0200
+++ b/src/HOL/Tools/function_package/fundef_core.ML	Sat Oct 13 17:16:39 2007 +0200
@@ -482,7 +482,7 @@
               |> Syntax.check_term lthy
 
       val ((f, (_, f_defthm)), lthy) =
-        LocalTheory.def Thm.internalK ((function_name fname, mixfix), ((fdefname, []), f_def)) lthy
+        LocalTheory.define Thm.internalK ((function_name fname, mixfix), ((fdefname, []), f_def)) lthy
     in
       ((f, f_defthm), lthy)
     end
diff -r 1a84a9ae9d58 -r 2bcac52d7abc src/HOL/Tools/function_package/mutual.ML
--- a/src/HOL/Tools/function_package/mutual.ML	Fri Oct 12 22:01:56 2007 +0200
+++ b/src/HOL/Tools/function_package/mutual.ML	Sat Oct 13 17:16:39 2007 +0200
@@ -184,7 +184,7 @@
       fun def ((MutualPart {i=i, i'=i', fvar=(fname, fT), cargTs, f_def, ...}), (_, mixfix)) lthy =
           let
             val ((f, (_, f_defthm)), lthy') =
-              LocalTheory.def Thm.internalK ((fname, mixfix),
+              LocalTheory.define Thm.internalK ((fname, mixfix),
                                             ((fname ^ "_def", []), Term.subst_bound (fsum, f_def)))
                               lthy
           in
diff -r 1a84a9ae9d58 -r 2bcac52d7abc src/HOL/Tools/inductive_package.ML
--- a/src/HOL/Tools/inductive_package.ML	Fri Oct 12 22:01:56 2007 +0200
+++ b/src/HOL/Tools/inductive_package.ML	Sat Oct 13 17:16:39 2007 +0200
@@ -645,7 +645,7 @@
       space_implode "_" (map fst cnames_syn) else alt_name;
 
     val ((rec_const, (_, fp_def)), ctxt') = ctxt |>
-      LocalTheory.def Thm.internalK
+      LocalTheory.define Thm.internalK
         ((rec_name, case cnames_syn of [(_, syn)] => syn | _ => NoSyn),
          (("", []), fold_rev lambda params
            (Const (fp_name, (predT --> predT) --> predT) $ fp_fun)));
@@ -662,7 +662,7 @@
             (list_comb (rec_const, params @ make_bool_args' bs i @
               make_args argTs (xs ~~ Ts)))))
         end) (cnames_syn ~~ cs);
-    val (consts_defs, ctxt'') = fold_map (LocalTheory.def Thm.internalK) specs ctxt';
+    val (consts_defs, ctxt'') = fold_map (LocalTheory.define Thm.internalK) specs ctxt';
     val preds = (case cs of [_] => [rec_const] | _ => map #1 consts_defs);
 
     val mono = prove_mono predT fp_fun monos ctxt''
diff -r 1a84a9ae9d58 -r 2bcac52d7abc src/HOL/Tools/inductive_set_package.ML
--- a/src/HOL/Tools/inductive_set_package.ML	Fri Oct 12 22:01:56 2007 +0200
+++ b/src/HOL/Tools/inductive_set_package.ML	Sat Oct 13 17:16:39 2007 +0200
@@ -468,7 +468,7 @@
         cs' intros' monos' params1 cnames_syn' ctxt;
 
     (* define inductive sets using previously defined predicates *)
-    val (defs, ctxt2) = fold_map (LocalTheory.def Thm.internalK)
+    val (defs, ctxt2) = fold_map (LocalTheory.define Thm.internalK)
       (map (fn ((c_syn, (fs, U, _)), p) => (c_syn, (("", []),
          fold_rev lambda params (HOLogic.Collect_const U $
            HOLogic.ap_split' fs U HOLogic.boolT (list_comb (p, params3))))))
diff -r 1a84a9ae9d58 -r 2bcac52d7abc src/Pure/Isar/instance.ML
--- a/src/Pure/Isar/instance.ML	Fri Oct 12 22:01:56 2007 +0200
+++ b/src/Pure/Isar/instance.ML	Sat Oct 13 17:16:39 2007 +0200
@@ -49,7 +49,7 @@
         pretty = LocalTheory.pretty,
         axioms = LocalTheory.axioms,
         abbrev = LocalTheory.abbrev,
-        def = LocalTheory.def,
+        define = LocalTheory.define,
         notes = LocalTheory.notes,
         type_syntax = LocalTheory.type_syntax,
         term_syntax = LocalTheory.term_syntax,
diff -r 1a84a9ae9d58 -r 2bcac52d7abc src/Pure/Isar/specification.ML
--- a/src/Pure/Isar/specification.ML	Fri Oct 12 22:01:56 2007 +0200
+++ b/src/Pure/Isar/specification.ML	Sat Oct 13 17:16:39 2007 +0200
@@ -165,7 +165,7 @@
       if x = x' then mx
       else error ("Head of definition " ^ quote x ^ " differs from declaration " ^ quote x'));
     val ((lhs, (_, th)), lthy2) = lthy
-      |> LocalTheory.def Thm.definitionK ((x, mx), ((name ^ "_raw", []), rhs));
+      |> LocalTheory.define Thm.definitionK ((x, mx), ((name ^ "_raw", []), rhs));
     val ((b, [th']), lthy3) = lthy2
       |> LocalTheory.note Thm.definitionK
           ((name, Code.add_default_func_attr :: atts), [prove lthy2 th]);