# HG changeset patch # User wenzelm # Date 1163620221 -3600 # Node ID b3a9d8a83dead74117e39d0ebfcbf71d632eae88 # Parent 10757dcdfe8031fcc8ab0447802f2122a9d2d388 replaced NameSpace.append by NameSpace.qualified, which handles empty names as expected; declared intro/elim rules; diff -r 10757dcdfe80 -r b3a9d8a83dea src/HOL/Tools/inductive_package.ML --- a/src/HOL/Tools/inductive_package.ML Wed Nov 15 17:05:48 2006 +0100 +++ b/src/HOL/Tools/inductive_package.ML Wed Nov 15 20:50:21 2006 +0100 @@ -658,20 +658,22 @@ val (intrs', ctxt2) = ctxt1 |> LocalTheory.notes - (map (NameSpace.append rec_name) intr_names ~~ + (map (NameSpace.qualified rec_name) intr_names ~~ intr_atts ~~ map (fn th => [([th], [])]) (ProofContext.export ctxt1 ctxt intrs)) |>> map (hd o snd); (* FIXME? *) val (((_, elims'), (_, [induct'])), ctxt3) = ctxt2 |> - LocalTheory.note ((NameSpace.append rec_name "intros", []), intrs') ||>> + LocalTheory.note ((NameSpace.qualified rec_name "intros", + [Attrib.internal (ContextRules.intro_query NONE)]), intrs') ||>> fold_map (fn (name, (elim, cases)) => - LocalTheory.note ((NameSpace.append (Sign.base_name name) "cases", + LocalTheory.note ((NameSpace.qualified (Sign.base_name name) "cases", [Attrib.internal (RuleCases.case_names cases), Attrib.internal (RuleCases.consumes 1), - Attrib.internal (InductAttrib.cases_set name)]), [elim]) #> + Attrib.internal (InductAttrib.cases_set name), + Attrib.internal (ContextRules.elim_query NONE)]), [elim]) #> apfst (hd o snd)) elims ||>> - LocalTheory.note ((NameSpace.append rec_name (coind_prefix coind ^ "induct"), + LocalTheory.note ((NameSpace.qualified rec_name (coind_prefix coind ^ "induct"), map Attrib.internal (#2 induct)), [rulify (#1 induct)]); val induct_att = if coind then InductAttrib.coinduct_set else InductAttrib.induct_set; @@ -683,7 +685,7 @@ [Attrib.internal ind_case_names, Attrib.internal (RuleCases.consumes 1), Attrib.internal (induct_att name)]), [([th], [])]))) |> snd |> - LocalTheory.note ((NameSpace.append rec_name (coind_prefix coind ^ "inducts"), + LocalTheory.note ((NameSpace.qualified rec_name (coind_prefix coind ^ "inducts"), [Attrib.internal ind_case_names, Attrib.internal (RuleCases.consumes 1)]), map snd inducts) |> snd end;