# HG changeset patch # User wenzelm # Date 1258638393 -3600 # Node ID c679f05600cd471056469080555fec274f13609a # Parent 47b5db0976469d7b75b282e1c6628717b0372a62 adapted Local_Theory.define -- eliminated odd thm kind; diff -r 47b5db097646 -r c679f05600cd src/HOL/Nominal/nominal_primrec.ML --- 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; diff -r 47b5db097646 -r c679f05600cd src/HOL/Tools/Function/function_core.ML --- 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 diff -r 47b5db097646 -r c679f05600cd src/HOL/Tools/Function/mutual.ML --- 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 diff -r 47b5db097646 -r c679f05600cd src/HOL/Tools/Function/size.ML --- 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; diff -r 47b5db097646 -r c679f05600cd src/HOL/Tools/inductive.ML --- 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); diff -r 47b5db097646 -r c679f05600cd src/HOL/Tools/inductive_set.ML --- 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)))))) diff -r 47b5db097646 -r c679f05600cd src/HOL/Tools/primrec.ML --- 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; diff -r 47b5db097646 -r c679f05600cd src/HOL/Tools/quickcheck_generators.ML --- 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; diff -r 47b5db097646 -r c679f05600cd src/HOLCF/Tools/fixrec.ML --- 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);