src/HOL/Tools/inductive_package.ML
changeset 18643 89a7978f90e1
parent 18463 56414918dbbd
child 18678 dd0c569fa43d
     1.1 --- a/src/HOL/Tools/inductive_package.ML	Tue Jan 10 19:33:42 2006 +0100
     1.2 +++ b/src/HOL/Tools/inductive_package.ML	Tue Jan 10 19:34:04 2006 +0100
     1.3 @@ -435,12 +435,12 @@
     1.4        thy
     1.5        |> Theory.parent_path
     1.6        |> Theory.add_path (Sign.base_name name)
     1.7 -      |> PureThy.add_thms [(("cases", elim), [InductAttrib.cases_set_global name])] |> snd
     1.8 +      |> PureThy.add_thms [(("cases", elim), [Attrib.theory (InductAttrib.cases_set name)])] |> snd
     1.9        |> Theory.restore_naming thy;
    1.10      val cases_specs = if no_elim then [] else map2 cases_spec names elims;
    1.11  
    1.12      val induct_att =
    1.13 -      if coind then InductAttrib.coinduct_set_global else InductAttrib.induct_set_global;
    1.14 +      Attrib.theory o (if coind then InductAttrib.coinduct_set else InductAttrib.induct_set);
    1.15      val induct_specs =
    1.16        if no_induct then I
    1.17        else