--- 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