# HG changeset patch # User wenzelm # Date 1258141289 -3600 # Node ID 02b7738aef6a341350bbae0fa35fe4921cf1bfb2 # Parent ae9a2ea9a98995911fbf29ff80c6ada2a30949f4 eliminated slightly odd kind argument of LocalTheory.note(s); added LocalTheory.notes_kind as fall-back for unusual cases; diff -r ae9a2ea9a989 -r 02b7738aef6a src/HOL/Nominal/nominal_inductive.ML --- a/src/HOL/Nominal/nominal_inductive.ML Fri Nov 13 19:57:46 2009 +0100 +++ b/src/HOL/Nominal/nominal_inductive.ML Fri Nov 13 20:41:29 2009 +0100 @@ -561,20 +561,19 @@ (strong_raw_induct, [ind_case_names, Rule_Cases.consumes 0]) else (strong_raw_induct RSN (2, rev_mp), [ind_case_names, Rule_Cases.consumes 1]); - val ((_, [strong_induct']), ctxt') = LocalTheory.note "" + val ((_, [strong_induct']), ctxt') = ctxt |> LocalTheory.note ((rec_qualified (Binding.name "strong_induct"), - map (Attrib.internal o K) (#2 strong_induct)), [#1 strong_induct]) - ctxt; + map (Attrib.internal o K) (#2 strong_induct)), [#1 strong_induct]); val strong_inducts = - Project_Rule.projects ctxt (1 upto length names) strong_induct' + Project_Rule.projects ctxt (1 upto length names) strong_induct'; in ctxt' |> - LocalTheory.note "" + LocalTheory.note ((rec_qualified (Binding.name "strong_inducts"), [Attrib.internal (K ind_case_names), Attrib.internal (K (Rule_Cases.consumes 1))]), strong_inducts) |> snd |> - LocalTheory.notes "" (map (fn ((name, elim), (_, cases)) => + LocalTheory.notes (map (fn ((name, elim), (_, cases)) => ((Binding.qualified_name (Long_Name.qualify (Long_Name.base_name name) "strong_cases"), [Attrib.internal (K (Rule_Cases.case_names (map snd cases))), Attrib.internal (K (Rule_Cases.consumes 1))]), [([elim], [])])) @@ -664,7 +663,7 @@ end) atoms in ctxt |> - LocalTheory.notes "" (map (fn (name, ths) => + LocalTheory.notes (map (fn (name, ths) => ((Binding.qualified_name (Long_Name.qualify (Long_Name.base_name name) "eqvt"), [Attrib.internal (K NominalThmDecls.eqvt_add)]), [(ths, [])])) (names ~~ transp thss)) |> snd diff -r ae9a2ea9a989 -r 02b7738aef6a src/HOL/Nominal/nominal_inductive2.ML --- a/src/HOL/Nominal/nominal_inductive2.ML Fri Nov 13 19:57:46 2009 +0100 +++ b/src/HOL/Nominal/nominal_inductive2.ML Fri Nov 13 20:41:29 2009 +0100 @@ -466,15 +466,14 @@ NONE => (rec_qualified (Binding.name "strong_induct"), rec_qualified (Binding.name "strong_inducts")) | SOME s => (Binding.name s, Binding.name (s ^ "s")); - val ((_, [strong_induct']), ctxt') = LocalTheory.note "" + val ((_, [strong_induct']), ctxt') = ctxt |> LocalTheory.note ((induct_name, - map (Attrib.internal o K) (#2 strong_induct)), [#1 strong_induct]) - ctxt; + map (Attrib.internal o K) (#2 strong_induct)), [#1 strong_induct]); val strong_inducts = Project_Rule.projects ctxt' (1 upto length names) strong_induct' in ctxt' |> - LocalTheory.note "" + LocalTheory.note ((inducts_name, [Attrib.internal (K ind_case_names), Attrib.internal (K (Rule_Cases.consumes 1))]), diff -r ae9a2ea9a989 -r 02b7738aef6a src/HOL/Nominal/nominal_primrec.ML --- a/src/HOL/Nominal/nominal_primrec.ML Fri Nov 13 19:57:46 2009 +0100 +++ b/src/HOL/Nominal/nominal_primrec.ML Fri Nov 13 20:41:29 2009 +0100 @@ -367,11 +367,10 @@ (fn thss => fn goal_ctxt => let val simps = ProofContext.export goal_ctxt lthy' (flat thss); - val (simps', lthy'') = fold_map (LocalTheory.note "") - (names_atts' ~~ map single simps) lthy' + val (simps', lthy'') = fold_map LocalTheory.note (names_atts' ~~ map single simps) lthy'; in lthy'' - |> LocalTheory.note "" ((qualify (Binding.name "simps"), + |> LocalTheory.note ((qualify (Binding.name "simps"), map (Attrib.internal o K) [Simplifier.simp_add, Nitpick_Simps.add]), maps snd simps') |> snd diff -r ae9a2ea9a989 -r 02b7738aef6a src/HOL/Tools/Function/function.ML --- a/src/HOL/Tools/Function/function.ML Fri Nov 13 19:57:46 2009 +0100 +++ b/src/HOL/Tools/Function/function.ML Fri Nov 13 20:41:29 2009 +0100 @@ -43,9 +43,6 @@ [Simplifier.simp_add, Nitpick_Psimps.add] -fun note_theorem ((binding, atts), ths) = - LocalTheory.note "" ((binding, atts), ths) - fun mk_defname fixes = fixes |> map (fst o fst) |> space_implode "_" fun add_simps fnames post sort extra_qualify label mod_binding moreatts simps lthy = @@ -55,13 +52,13 @@ |> map (apfst (apfst extra_qualify)) val (saved_spec_simps, lthy) = - fold_map (LocalTheory.note "") spec lthy + fold_map LocalTheory.note spec lthy val saved_simps = maps snd saved_spec_simps val simps_by_f = sort saved_simps fun add_for_f fname simps = - note_theorem ((mod_binding (Binding.qualify true fname (Binding.name label)), []), simps) + LocalTheory.note ((mod_binding (Binding.qualify true fname (Binding.name label)), []), simps) #> snd in (saved_simps, @@ -100,14 +97,14 @@ |> addsmps (conceal_partial o Binding.qualify false "partial") "psimps" conceal_partial psimp_attribs psimps ||> fold_option (snd oo addsmps I "simps" I simp_attribs) trsimps - ||>> note_theorem ((conceal_partial (qualify "pinduct"), + ||>> LocalTheory.note ((conceal_partial (qualify "pinduct"), [Attrib.internal (K (Rule_Cases.case_names cnames)), Attrib.internal (K (Rule_Cases.consumes 1)), Attrib.internal (K (Induct.induct_pred ""))]), simple_pinducts) - ||>> note_theorem ((Binding.conceal (qualify "termination"), []), [termination]) - ||> (snd o note_theorem ((qualify "cases", + ||>> LocalTheory.note ((Binding.conceal (qualify "termination"), []), [termination]) + ||> (snd o LocalTheory.note ((qualify "cases", [Attrib.internal (K (Rule_Cases.case_names cnames))]), [cases])) - ||> fold_option (snd oo curry note_theorem (qualify "domintros", [])) domintros + ||> fold_option (snd oo curry LocalTheory.note (qualify "domintros", [])) domintros val cdata = FunctionCtxData { add_simps=addsmps, case_names=cnames, psimps=psimps', pinducts=snd pinducts', termination=termination', @@ -155,7 +152,7 @@ in lthy |> add_simps I "simps" I simp_attribs tsimps |> snd - |> note_theorem + |> LocalTheory.note ((qualify "induct", [Attrib.internal (K (Rule_Cases.case_names case_names))]), tinduct) |> snd diff -r ae9a2ea9a989 -r 02b7738aef6a src/HOL/Tools/inductive.ML --- a/src/HOL/Tools/inductive.ML Fri Nov 13 19:57:46 2009 +0100 +++ b/src/HOL/Tools/inductive.ML Fri Nov 13 20:41:29 2009 +0100 @@ -469,7 +469,7 @@ val facts = args |> map (fn ((a, atts), props) => ((a, map (prep_att thy) atts), map (Thm.no_attributes o single o mk_cases lthy o prep_prop lthy) props)); - in lthy |> LocalTheory.notes "" facts |>> map snd end; + in lthy |> LocalTheory.notes facts |>> map snd end; val inductive_cases = gen_inductive_cases Attrib.intern_src Syntax.read_prop; val inductive_cases_i = gen_inductive_cases (K I) Syntax.check_prop; @@ -695,7 +695,7 @@ val mono = prove_mono quiet_mode skip_mono fork_mono predT fp_fun monos lthy''; val ((_, [mono']), lthy''') = - LocalTheory.note "" (apfst Binding.conceal Attrib.empty_binding, [mono]) lthy''; + LocalTheory.note (apfst Binding.conceal Attrib.empty_binding, [mono]) lthy''; in (lthy''', rec_name, mono', fp_def', map (#2 o #2) consts_defs, list_comb (rec_const, params), preds, argTs, bs, xs) @@ -719,7 +719,7 @@ val (intrs', lthy1) = lthy |> - LocalTheory.notes "" + LocalTheory.notes (map (rec_qualified false) intr_bindings ~~ intr_atts ~~ map (fn th => [([th], [Attrib.internal (K (Context_Rules.intro_query NONE)), @@ -727,16 +727,16 @@ map (hd o snd); val (((_, elims'), (_, [induct'])), lthy2) = lthy1 |> - LocalTheory.note "" ((rec_qualified true (Binding.name "intros"), []), intrs') ||>> + LocalTheory.note ((rec_qualified true (Binding.name "intros"), []), intrs') ||>> fold_map (fn (name, (elim, cases)) => - LocalTheory.note "" + LocalTheory.note ((Binding.qualify true (Long_Name.base_name name) (Binding.name "cases"), [Attrib.internal (K (Rule_Cases.case_names cases)), Attrib.internal (K (Rule_Cases.consumes 1)), Attrib.internal (K (Induct.cases_pred name)), Attrib.internal (K (Context_Rules.elim_query NONE))]), [elim]) #> apfst (hd o snd)) (if null elims then [] else cnames ~~ elims) ||>> - LocalTheory.note "" + LocalTheory.note ((rec_qualified true (Binding.name (coind_prefix coind ^ "induct")), map (Attrib.internal o K) (#2 induct)), [rulify (#1 induct)]); @@ -745,7 +745,7 @@ else let val inducts = cnames ~~ Project_Rule.projects lthy2 (1 upto length cnames) induct' in lthy2 |> - LocalTheory.notes "" [((rec_qualified true (Binding.name "inducts"), []), + LocalTheory.notes [((rec_qualified true (Binding.name "inducts"), []), inducts |> map (fn (name, th) => ([th], [Attrib.internal (K ind_case_names), Attrib.internal (K (Rule_Cases.consumes 1)), diff -r ae9a2ea9a989 -r 02b7738aef6a src/HOL/Tools/inductive_set.ML --- a/src/HOL/Tools/inductive_set.ML Fri Nov 13 19:57:46 2009 +0100 +++ b/src/HOL/Tools/inductive_set.ML Fri Nov 13 20:41:29 2009 +0100 @@ -505,7 +505,7 @@ (K (REPEAT (rtac ext 1) THEN simp_tac (HOL_basic_ss addsimps [def, mem_Collect_eq, split_conv]) 1)) in - lthy |> LocalTheory.note "" ((Binding.name (s ^ "p_" ^ s ^ "_eq"), + lthy |> LocalTheory.note ((Binding.name (s ^ "p_" ^ s ^ "_eq"), [Attrib.internal (K pred_set_conv_att)]), [conv_thm]) |> snd end) (preds ~~ cs ~~ cs_info ~~ defs) lthy2; diff -r ae9a2ea9a989 -r 02b7738aef6a src/HOL/Tools/primrec.ML --- a/src/HOL/Tools/primrec.ML Fri Nov 13 19:57:46 2009 +0100 +++ b/src/HOL/Tools/primrec.ML Fri Nov 13 20:41:29 2009 +0100 @@ -277,8 +277,8 @@ lthy |> set_group ? LocalTheory.set_group (serial ()) |> add_primrec_simple fixes (map snd spec) - |-> (fn (prefix, simps) => fold_map (LocalTheory.note "") (attr_bindings prefix ~~ simps) - #-> (fn simps' => LocalTheory.note "" (simp_attr_binding prefix, maps snd simps'))) + |-> (fn (prefix, simps) => fold_map LocalTheory.note (attr_bindings prefix ~~ simps) + #-> (fn simps' => LocalTheory.note (simp_attr_binding prefix, maps snd simps'))) |>> snd end; diff -r ae9a2ea9a989 -r 02b7738aef6a src/HOL/Tools/quickcheck_generators.ML --- a/src/HOL/Tools/quickcheck_generators.ML Fri Nov 13 19:57:46 2009 +0100 +++ b/src/HOL/Tools/quickcheck_generators.ML Fri Nov 13 20:41:29 2009 +0100 @@ -214,7 +214,7 @@ lthy |> random_aux_primrec_multi (name ^ prfx) proto_eqs |-> (fn proto_simps => prove_simps proto_simps) - |-> (fn simps => LocalTheory.note "" + |-> (fn simps => LocalTheory.note ((b, Code.add_default_eqn_attrib :: map (Attrib.internal o K) [Simplifier.simp_add, Nitpick_Simps.add]), simps)) |> snd diff -r ae9a2ea9a989 -r 02b7738aef6a src/HOLCF/Tools/fixrec.ML --- a/src/HOLCF/Tools/fixrec.ML Fri Nov 13 19:57:46 2009 +0100 +++ b/src/HOLCF/Tools/fixrec.ML Fri Nov 13 20:41:29 2009 +0100 @@ -242,7 +242,7 @@ ((thm_name, [src]), [thm]) end; val (thmss, lthy'') = lthy' - |> fold_map (LocalTheory.note "") (induct_note :: map unfold_note unfold_thms); + |> fold_map LocalTheory.note (induct_note :: map unfold_note unfold_thms); in (lthy'', names, fixdef_thms, map snd unfold_thms) end; @@ -464,7 +464,7 @@ val simps2 : (Attrib.binding * thm list) list = map (apsnd (fn thm => [thm])) (flat simps); val (_, lthy'') = lthy' - |> fold_map (LocalTheory.note "") (simps1 @ simps2); + |> fold_map LocalTheory.note (simps1 @ simps2); in lthy'' end diff -r ae9a2ea9a989 -r 02b7738aef6a src/Pure/Isar/expression.ML --- a/src/Pure/Isar/expression.ML Fri Nov 13 19:57:46 2009 +0100 +++ b/src/Pure/Isar/expression.ML Fri Nov 13 20:41:29 2009 +0100 @@ -775,7 +775,7 @@ |> Locale.register_locale binding (extraTs, params) (asm, rev defs) (a_intro, b_intro) axioms ([], []) (rev notes) (rev deps') |> Theory_Target.init (SOME name) - |> fold (fn (kind, facts) => LocalTheory.notes kind facts #> snd) notes'; + |> fold (fn (kind, facts) => LocalTheory.notes_kind kind facts #> snd) notes'; in (name, loc_ctxt) end; diff -r ae9a2ea9a989 -r 02b7738aef6a src/Pure/Isar/local_theory.ML --- a/src/Pure/Isar/local_theory.ML Fri Nov 13 19:57:46 2009 +0100 +++ b/src/Pure/Isar/local_theory.ML Fri Nov 13 20:41:29 2009 +0100 @@ -33,8 +33,10 @@ (term * term) * local_theory val define: string -> (binding * mixfix) * (Attrib.binding * term) -> local_theory -> (term * (string * thm)) * local_theory - val note: string -> Attrib.binding * thm list -> local_theory -> (string * thm list) * local_theory - val notes: string -> (Attrib.binding * (thm list * Attrib.src list) list) list -> + val note: Attrib.binding * thm list -> local_theory -> (string * thm list) * local_theory + val notes: (Attrib.binding * (thm list * Attrib.src list) list) list -> + local_theory -> (string * thm list) list * local_theory + val notes_kind: string -> (Attrib.binding * (thm list * Attrib.src list) list) list -> local_theory -> (string * thm list) list * local_theory val type_syntax: bool -> declaration -> local_theory -> local_theory val term_syntax: bool -> declaration -> local_theory -> local_theory @@ -186,12 +188,13 @@ val pretty = operation #pretty; val abbrev = apsnd checkpoint ooo operation2 #abbrev; val define = apsnd checkpoint ooo operation2 #define; -val notes = apsnd checkpoint ooo operation2 #notes; +val notes_kind = apsnd checkpoint ooo operation2 #notes; val type_syntax = checkpoint ooo operation2 #type_syntax; val term_syntax = checkpoint ooo operation2 #term_syntax; val declaration = checkpoint ooo operation2 #declaration; -fun note kind (a, ths) = notes kind [(a, [(ths, [])])] #>> the_single; +val notes = notes_kind ""; +fun note (a, ths) = notes [(a, [(ths, [])])] #>> the_single; fun notation add mode raw_args lthy = let val args = map (apfst (Morphism.term (target_morphism lthy))) raw_args diff -r ae9a2ea9a989 -r 02b7738aef6a src/Pure/Isar/specification.ML --- a/src/Pure/Isar/specification.ML Fri Nov 13 19:57:46 2009 +0100 +++ b/src/Pure/Isar/specification.ML Fri Nov 13 20:41:29 2009 +0100 @@ -208,10 +208,10 @@ val th = prove lthy2 raw_th; val lthy3 = lthy2 |> Spec_Rules.add Spec_Rules.Equational ([lhs], [th]); - val ((def_name, [th']), lthy4) = lthy3 - |> LocalTheory.note Thm.definitionK - ((name, Predicate_Compile_Preproc_Const_Defs.add_attrib :: - Code.add_default_eqn_attrib :: atts), [th]); + val ([(def_name, [th'])], lthy4) = lthy3 + |> LocalTheory.notes_kind Thm.definitionK + [((name, Predicate_Compile_Preproc_Const_Defs.add_attrib :: + Code.add_default_eqn_attrib :: atts), [([th], [])])]; val lhs' = Morphism.term (LocalTheory.target_morphism lthy4) lhs; val _ = @@ -270,7 +270,7 @@ val facts = raw_facts |> map (fn ((name, atts), bs) => ((name, map attrib atts), bs |> map (fn (b, more_atts) => (prep_fact lthy b, map attrib more_atts)))); - val (res, lthy') = lthy |> LocalTheory.notes kind facts; + val (res, lthy') = lthy |> LocalTheory.notes_kind kind facts; val _ = Proof_Display.print_results true lthy' ((kind, ""), res); in (res, lthy') end; @@ -359,14 +359,15 @@ burrow (map Goal.norm_result o ProofContext.export goal_ctxt' lthy) results in lthy - |> LocalTheory.notes kind (map2 (fn (a, _) => fn ths => (a, [(ths, [])])) stmt results') + |> LocalTheory.notes_kind kind + (map2 (fn (a, _) => fn ths => (a, [(ths, [])])) stmt results') |> (fn (res, lthy') => if Binding.is_empty name andalso null atts then (Proof_Display.print_results true lthy' ((kind, ""), res); lthy') else let val ([(res_name, _)], lthy'') = lthy' - |> LocalTheory.notes kind [((name, atts), [(maps #2 res, [])])]; + |> LocalTheory.notes_kind kind [((name, atts), [(maps #2 res, [])])]; val _ = Proof_Display.print_results true lthy' ((kind, res_name), res); in lthy'' end) |> after_qed results' diff -r ae9a2ea9a989 -r 02b7738aef6a src/Pure/Isar/theory_target.ML --- a/src/Pure/Isar/theory_target.ML Fri Nov 13 19:57:46 2009 +0100 +++ b/src/Pure/Isar/theory_target.ML Fri Nov 13 20:41:29 2009 +0100 @@ -310,7 +310,8 @@ local fun init_target _ NONE = global_target - | init_target thy (SOME target) = if Locale.defined thy (Locale.intern thy target) + | init_target thy (SOME target) = + if Locale.defined thy (Locale.intern thy target) then make_target target true (Class_Target.is_class thy target) ([], [], []) [] else error ("No such locale: " ^ quote target);