adapted Local_Theory.define -- eliminated odd thm kind;

--- a/src/HOL/Nominal/nominal_primrec.ML	Thu Nov 19 14:45:56 2009 +0100
+++ b/src/HOL/Nominal/nominal_primrec.ML	Thu Nov 19 14:46:33 2009 +0100
@@ -280,7 +280,7 @@
       else primrec_err ("functions " ^ commas_quote names2 ^
         "\nare not mutually recursive");
     val (defs_thms, lthy') = lthy |>
-      fold_map (apfst (snd o snd) oo Local_Theory.define Thm.definitionK o fst) defs';
+      fold_map (apfst (snd o snd) oo Local_Theory.define o fst) defs';
     val qualify = Binding.qualify false
       (space_implode "_" (map (Long_Name.base_name o #1) defs));
     val names_atts' = map (apfst qualify) names_atts;

--- a/src/HOL/Tools/Function/function_core.ML	Thu Nov 19 14:45:56 2009 +0100
+++ b/src/HOL/Tools/Function/function_core.ML	Thu Nov 19 14:46:33 2009 +0100
@@ -518,7 +518,7 @@
         $ (default $ Bound 0) $ Abs ("y", ranT, G $ Bound 1 $ Bound 0))
       |> Syntax.check_term lthy
   in
-    Local_Theory.define ""
+    Local_Theory.define
       ((Binding.name (function_name fname), mixfix),
         ((Binding.conceal (Binding.name fdefname), []), f_def)) lthy
   end

--- a/src/HOL/Tools/Function/mutual.ML	Thu Nov 19 14:45:56 2009 +0100
+++ b/src/HOL/Tools/Function/mutual.ML	Thu Nov 19 14:46:33 2009 +0100
@@ -146,7 +146,7 @@
       fun def ((MutualPart {i=i, i'=i', fvar=(fname, fT), cargTs, f_def, ...}), (_, mixfix)) lthy =
           let
             val ((f, (_, f_defthm)), lthy') =
-              Local_Theory.define ""
+              Local_Theory.define
                 ((Binding.name fname, mixfix),
                   ((Binding.conceal (Binding.name (fname ^ "_def")), []),
                   Term.subst_bound (fsum, f_def))) lthy

--- a/src/HOL/Tools/Function/size.ML	Thu Nov 19 14:45:56 2009 +0100
+++ b/src/HOL/Tools/Function/size.ML	Thu Nov 19 14:46:33 2009 +0100
@@ -130,8 +130,8 @@
     fun define_overloaded (def_name, eq) lthy =
       let
         val (Free (c, _), rhs) = (Logic.dest_equals o Syntax.check_term lthy) eq;
-        val ((_, (_, thm)), lthy') = lthy |> Local_Theory.define Thm.definitionK
-          ((Binding.name c, NoSyn), ((Binding.name def_name, []), rhs));
+        val ((_, (_, thm)), lthy') = lthy
+          |> Local_Theory.define ((Binding.name c, NoSyn), ((Binding.name def_name, []), rhs));
         val ctxt_thy = ProofContext.init (ProofContext.theory_of lthy');
         val thm' = singleton (ProofContext.export lthy' ctxt_thy) thm;
       in (thm', lthy') end;

--- a/src/HOL/Tools/inductive.ML	Thu Nov 19 14:45:56 2009 +0100
+++ b/src/HOL/Tools/inductive.ML	Thu Nov 19 14:46:33 2009 +0100
@@ -666,7 +666,7 @@
 
     val ((rec_const, (_, fp_def)), lthy') = lthy
       |> Local_Theory.conceal
-      |> Local_Theory.define ""
+      |> Local_Theory.define
         ((rec_name, case cnames_syn of [(_, syn)] => syn | _ => NoSyn),
          ((Binding.empty, [Attrib.internal (K Nitpick_Defs.add)]),
          fold_rev lambda params
@@ -689,7 +689,7 @@
           end) (cnames_syn ~~ cs);
     val (consts_defs, lthy'') = lthy'
       |> Local_Theory.conceal
-      |> fold_map (Local_Theory.define "") specs
+      |> fold_map Local_Theory.define specs
       ||> Local_Theory.restore_naming lthy';
     val preds = (case cs of [_] => [rec_const] | _ => map #1 consts_defs);
 

--- a/src/HOL/Tools/inductive_set.ML	Thu Nov 19 14:45:56 2009 +0100
+++ b/src/HOL/Tools/inductive_set.ML	Thu Nov 19 14:46:33 2009 +0100
@@ -485,7 +485,7 @@
     (* define inductive sets using previously defined predicates *)
     val (defs, lthy2) = lthy1
       |> Local_Theory.conceal  (* FIXME ?? *)
-      |> fold_map (Local_Theory.define "")
+      |> fold_map Local_Theory.define
         (map (fn ((c_syn, (fs, U, _)), p) => (c_syn, (Attrib.empty_binding,
            fold_rev lambda params (HOLogic.Collect_const U $
              HOLogic.mk_psplits fs U HOLogic.boolT (list_comb (p, params3))))))

--- a/src/HOL/Tools/primrec.ML	Thu Nov 19 14:45:56 2009 +0100
+++ b/src/HOL/Tools/primrec.ML	Thu Nov 19 14:46:33 2009 +0100
@@ -259,7 +259,7 @@
     val ((prefix, (fs, defs)), prove) = distill lthy fixes ts;
   in
     lthy
-    |> fold_map (Local_Theory.define Thm.definitionK) defs
+    |> fold_map Local_Theory.define defs
     |-> (fn defs => `(fn lthy => (prefix, prove lthy defs)))
   end;
 

--- a/src/HOL/Tools/quickcheck_generators.ML	Thu Nov 19 14:45:56 2009 +0100
+++ b/src/HOL/Tools/quickcheck_generators.ML	Thu Nov 19 14:46:33 2009 +0100
@@ -190,7 +190,7 @@
       in
         lthy
         |> random_aux_primrec aux_eq'
-        ||>> fold_map (Local_Theory.define Thm.definitionK) proj_defs
+        ||>> fold_map Local_Theory.define proj_defs
         |-> (fn (aux_simp, proj_defs) => prove_eqs aux_simp proj_defs)
       end;
 

--- a/src/HOLCF/Tools/fixrec.ML	Thu Nov 19 14:45:56 2009 +0100
+++ b/src/HOLCF/Tools/fixrec.ML	Thu Nov 19 14:46:33 2009 +0100
@@ -209,9 +209,8 @@
       | defs (l::[]) r = [one_def l r]
       | defs (l::ls) r = one_def l (mk_fst r) :: defs ls (mk_snd r);
     val fixdefs = defs lhss fixpoint;
-    val define_all = fold_map (Local_Theory.define Thm.definitionK);
     val (fixdef_thms : (term * (string * thm)) list, lthy') = lthy
-      |> define_all (map (apfst fst) fixes ~~ fixdefs);
+      |> fold_map Local_Theory.define (map (apfst fst) fixes ~~ fixdefs);
     fun pair_equalI (thm1, thm2) = @{thm Pair_equalI} OF [thm1, thm2];
     val tuple_fixdef_thm = foldr1 pair_equalI (map (snd o snd) fixdef_thms);
     val P = Var (("P", 0), map Term.fastype_of lhss ---> HOLogic.boolT);