# HG changeset patch # User krauss # Date 1257197040 -3600 # Node ID 9c6980f2eb39d23e6c2d98087cbed6e3b21ed298 # Parent 2240b0e7fa101ba2ea4c631205daa5e0fe357e45 conceal "termination" rule, used only by special tools diff -r 2240b0e7fa10 -r 9c6980f2eb39 src/HOL/Tools/Function/function.ML --- a/src/HOL/Tools/Function/function.ML Mon Nov 02 22:23:57 2009 +0100 +++ b/src/HOL/Tools/Function/function.ML Mon Nov 02 22:24:00 2009 +0100 @@ -44,8 +44,8 @@ [Simplifier.simp_add, Nitpick_Psimps.add] -fun note_theorem ((name, atts), ths) = - LocalTheory.note Thm.generatedK ((Binding.qualified_name name, atts), ths) +fun note_theorem ((binding, atts), ths) = + LocalTheory.note Thm.generatedK ((binding, atts), ths) fun mk_defname fixes = fixes |> map (fst o fst) |> space_implode "_" @@ -62,7 +62,8 @@ val simps_by_f = sort saved_simps fun add_for_f fname simps = - note_theorem ((Long_Name.qualify fname label, []), simps) #> snd + note_theorem ((Binding.qualified_name (Long_Name.qualify fname label), []), simps) + #> snd in (saved_simps, fold2 add_for_f fnames simps_by_f lthy) @@ -89,7 +90,9 @@ cont (Thm.close_derivation proof) val fnames = map (fst o fst) fixes - val qualify = Long_Name.qualify defname + fun qualify n = Binding.name n + |> Binding.qualify true defname + val addsmps = add_simps fnames post sort_cont val (((psimps', pinducts'), (_, [termination'])), lthy) = @@ -101,7 +104,7 @@ [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 ((qualify "termination", []), [termination]) + ||>> note_theorem ((Binding.conceal (qualify "termination"), []), [termination]) ||> (snd o note_theorem ((qualify "cases", [Attrib.internal (K (Rule_Cases.case_names cnames))]), [cases])) ||> fold_option (snd oo curry note_theorem (qualify "domintros", [])) domintros @@ -147,7 +150,8 @@ full_simplify (HOL_basic_ss addsimps [totality, True_implies_equals]) val tsimps = map remove_domain_condition psimps val tinduct = map remove_domain_condition pinducts - val qualify = Long_Name.qualify defname; + fun qualify n = Binding.name n + |> Binding.qualify true defname in lthy |> add_simps I "simps" simp_attribs tsimps |> snd