adapted Local_Theory.define -- eliminated odd thm kind;
authorwenzelm
Thu Nov 19 14:46:33 2009 +0100 (2009-11-19)
changeset 33766c679f05600cd
parent 33765 47b5db097646
child 33767 f962c761a38f
adapted Local_Theory.define -- eliminated odd thm kind;
src/HOL/Nominal/nominal_primrec.ML
src/HOL/Tools/Function/function_core.ML
src/HOL/Tools/Function/mutual.ML
src/HOL/Tools/Function/size.ML
src/HOL/Tools/inductive.ML
src/HOL/Tools/inductive_set.ML
src/HOL/Tools/primrec.ML
src/HOL/Tools/quickcheck_generators.ML
src/HOLCF/Tools/fixrec.ML
     1.1 --- a/src/HOL/Nominal/nominal_primrec.ML	Thu Nov 19 14:45:56 2009 +0100
     1.2 +++ b/src/HOL/Nominal/nominal_primrec.ML	Thu Nov 19 14:46:33 2009 +0100
     1.3 @@ -280,7 +280,7 @@
     1.4        else primrec_err ("functions " ^ commas_quote names2 ^
     1.5          "\nare not mutually recursive");
     1.6      val (defs_thms, lthy') = lthy |>
     1.7 -      fold_map (apfst (snd o snd) oo Local_Theory.define Thm.definitionK o fst) defs';
     1.8 +      fold_map (apfst (snd o snd) oo Local_Theory.define o fst) defs';
     1.9      val qualify = Binding.qualify false
    1.10        (space_implode "_" (map (Long_Name.base_name o #1) defs));
    1.11      val names_atts' = map (apfst qualify) names_atts;
     2.1 --- a/src/HOL/Tools/Function/function_core.ML	Thu Nov 19 14:45:56 2009 +0100
     2.2 +++ b/src/HOL/Tools/Function/function_core.ML	Thu Nov 19 14:46:33 2009 +0100
     2.3 @@ -518,7 +518,7 @@
     2.4          $ (default $ Bound 0) $ Abs ("y", ranT, G $ Bound 1 $ Bound 0))
     2.5        |> Syntax.check_term lthy
     2.6    in
     2.7 -    Local_Theory.define ""
     2.8 +    Local_Theory.define
     2.9        ((Binding.name (function_name fname), mixfix),
    2.10          ((Binding.conceal (Binding.name fdefname), []), f_def)) lthy
    2.11    end
     3.1 --- a/src/HOL/Tools/Function/mutual.ML	Thu Nov 19 14:45:56 2009 +0100
     3.2 +++ b/src/HOL/Tools/Function/mutual.ML	Thu Nov 19 14:46:33 2009 +0100
     3.3 @@ -146,7 +146,7 @@
     3.4        fun def ((MutualPart {i=i, i'=i', fvar=(fname, fT), cargTs, f_def, ...}), (_, mixfix)) lthy =
     3.5            let
     3.6              val ((f, (_, f_defthm)), lthy') =
     3.7 -              Local_Theory.define ""
     3.8 +              Local_Theory.define
     3.9                  ((Binding.name fname, mixfix),
    3.10                    ((Binding.conceal (Binding.name (fname ^ "_def")), []),
    3.11                    Term.subst_bound (fsum, f_def))) lthy
     4.1 --- a/src/HOL/Tools/Function/size.ML	Thu Nov 19 14:45:56 2009 +0100
     4.2 +++ b/src/HOL/Tools/Function/size.ML	Thu Nov 19 14:46:33 2009 +0100
     4.3 @@ -130,8 +130,8 @@
     4.4      fun define_overloaded (def_name, eq) lthy =
     4.5        let
     4.6          val (Free (c, _), rhs) = (Logic.dest_equals o Syntax.check_term lthy) eq;
     4.7 -        val ((_, (_, thm)), lthy') = lthy |> Local_Theory.define Thm.definitionK
     4.8 -          ((Binding.name c, NoSyn), ((Binding.name def_name, []), rhs));
     4.9 +        val ((_, (_, thm)), lthy') = lthy
    4.10 +          |> Local_Theory.define ((Binding.name c, NoSyn), ((Binding.name def_name, []), rhs));
    4.11          val ctxt_thy = ProofContext.init (ProofContext.theory_of lthy');
    4.12          val thm' = singleton (ProofContext.export lthy' ctxt_thy) thm;
    4.13        in (thm', lthy') end;
     5.1 --- a/src/HOL/Tools/inductive.ML	Thu Nov 19 14:45:56 2009 +0100
     5.2 +++ b/src/HOL/Tools/inductive.ML	Thu Nov 19 14:46:33 2009 +0100
     5.3 @@ -666,7 +666,7 @@
     5.4  
     5.5      val ((rec_const, (_, fp_def)), lthy') = lthy
     5.6        |> Local_Theory.conceal
     5.7 -      |> Local_Theory.define ""
     5.8 +      |> Local_Theory.define
     5.9          ((rec_name, case cnames_syn of [(_, syn)] => syn | _ => NoSyn),
    5.10           ((Binding.empty, [Attrib.internal (K Nitpick_Defs.add)]),
    5.11           fold_rev lambda params
    5.12 @@ -689,7 +689,7 @@
    5.13            end) (cnames_syn ~~ cs);
    5.14      val (consts_defs, lthy'') = lthy'
    5.15        |> Local_Theory.conceal
    5.16 -      |> fold_map (Local_Theory.define "") specs
    5.17 +      |> fold_map Local_Theory.define specs
    5.18        ||> Local_Theory.restore_naming lthy';
    5.19      val preds = (case cs of [_] => [rec_const] | _ => map #1 consts_defs);
    5.20  
     6.1 --- a/src/HOL/Tools/inductive_set.ML	Thu Nov 19 14:45:56 2009 +0100
     6.2 +++ b/src/HOL/Tools/inductive_set.ML	Thu Nov 19 14:46:33 2009 +0100
     6.3 @@ -485,7 +485,7 @@
     6.4      (* define inductive sets using previously defined predicates *)
     6.5      val (defs, lthy2) = lthy1
     6.6        |> Local_Theory.conceal  (* FIXME ?? *)
     6.7 -      |> fold_map (Local_Theory.define "")
     6.8 +      |> fold_map Local_Theory.define
     6.9          (map (fn ((c_syn, (fs, U, _)), p) => (c_syn, (Attrib.empty_binding,
    6.10             fold_rev lambda params (HOLogic.Collect_const U $
    6.11               HOLogic.mk_psplits fs U HOLogic.boolT (list_comb (p, params3))))))
     7.1 --- a/src/HOL/Tools/primrec.ML	Thu Nov 19 14:45:56 2009 +0100
     7.2 +++ b/src/HOL/Tools/primrec.ML	Thu Nov 19 14:46:33 2009 +0100
     7.3 @@ -259,7 +259,7 @@
     7.4      val ((prefix, (fs, defs)), prove) = distill lthy fixes ts;
     7.5    in
     7.6      lthy
     7.7 -    |> fold_map (Local_Theory.define Thm.definitionK) defs
     7.8 +    |> fold_map Local_Theory.define defs
     7.9      |-> (fn defs => `(fn lthy => (prefix, prove lthy defs)))
    7.10    end;
    7.11  
     8.1 --- a/src/HOL/Tools/quickcheck_generators.ML	Thu Nov 19 14:45:56 2009 +0100
     8.2 +++ b/src/HOL/Tools/quickcheck_generators.ML	Thu Nov 19 14:46:33 2009 +0100
     8.3 @@ -190,7 +190,7 @@
     8.4        in
     8.5          lthy
     8.6          |> random_aux_primrec aux_eq'
     8.7 -        ||>> fold_map (Local_Theory.define Thm.definitionK) proj_defs
     8.8 +        ||>> fold_map Local_Theory.define proj_defs
     8.9          |-> (fn (aux_simp, proj_defs) => prove_eqs aux_simp proj_defs)
    8.10        end;
    8.11  
     9.1 --- a/src/HOLCF/Tools/fixrec.ML	Thu Nov 19 14:45:56 2009 +0100
     9.2 +++ b/src/HOLCF/Tools/fixrec.ML	Thu Nov 19 14:46:33 2009 +0100
     9.3 @@ -209,9 +209,8 @@
     9.4        | defs (l::[]) r = [one_def l r]
     9.5        | defs (l::ls) r = one_def l (mk_fst r) :: defs ls (mk_snd r);
     9.6      val fixdefs = defs lhss fixpoint;
     9.7 -    val define_all = fold_map (Local_Theory.define Thm.definitionK);
     9.8      val (fixdef_thms : (term * (string * thm)) list, lthy') = lthy
     9.9 -      |> define_all (map (apfst fst) fixes ~~ fixdefs);
    9.10 +      |> fold_map Local_Theory.define (map (apfst fst) fixes ~~ fixdefs);
    9.11      fun pair_equalI (thm1, thm2) = @{thm Pair_equalI} OF [thm1, thm2];
    9.12      val tuple_fixdef_thm = foldr1 pair_equalI (map (snd o snd) fixdef_thms);
    9.13      val P = Var (("P", 0), map Term.fastype_of lhss ---> HOLogic.boolT);