1.1 --- a/src/HOLCF/Tools/domain/domain_theorems.ML	Tue Mar 31 22:25:46 2009 +0200
     1.2 +++ b/src/HOLCF/Tools/domain/domain_theorems.ML	Tue Mar 31 15:57:10 2009 -0700
     1.3 @@ -610,7 +610,7 @@
     1.4      |> (snd o PureThy.add_thmss [
     1.5          ((Binding.name "iso_rews" , iso_rews  ), [Simplifier.simp_add]),
     1.6          ((Binding.name "exhaust"  , [exhaust] ), []),
     1.7 -        ((Binding.name "casedist" , [casedist]), [Induct.cases_type (Long_Name.base_name dname)]),
     1.8 +        ((Binding.name "casedist" , [casedist]), [Induct.cases_type dname]),
     1.9          ((Binding.name "when_rews", when_rews ), [Simplifier.simp_add]),
    1.10          ((Binding.name "compacts", con_compacts), [Simplifier.simp_add]),
    1.11          ((Binding.name "con_rews", con_rews), [Simplifier.simp_add]),
    1.12 @@ -999,6 +999,9 @@
    1.13      in pg [] goal (K tacs) end;
    1.14  end; (* local *)
    1.15  
    1.16 +val inducts = ProjectRule.projections (ProofContext.init thy) ind;
    1.17 +fun ind_rule (dname, rule) = ((Binding.empty, [rule]), [Induct.induct_type dname]);
    1.18 +
    1.19  in thy |> Sign.add_path comp_dnam
    1.20         |> (snd o (PureThy.add_thmss (map (Thm.no_attributes o apfst Binding.name) [
    1.21  		("take_rews"  , take_rews  ),
    1.22 @@ -1007,6 +1010,7 @@
    1.23  		("finite_ind", [finite_ind]),
    1.24  		("ind"       , [ind       ]),
    1.25  		("coind"     , [coind     ])])))
    1.26 +       |> (snd o (PureThy.add_thmss (map ind_rule (dnames ~~ inducts))))
    1.27         |> Sign.parent_path |> pair take_rews
    1.28  end; (* let *)
    1.29  end; (* local *)