# HG changeset patch
# User huffman
# Date 1238540230 25200
# Node ID d64a293f23ba8a923ef4d47450ab7258d0960d9d
# Parent  50c8f55cde7ff9f2a3df6ec65ef02665e2c7ee3c
domain package registers induction rules

diff -r 50c8f55cde7f -r d64a293f23ba src/HOLCF/Tools/domain/domain_theorems.ML
--- a/src/HOLCF/Tools/domain/domain_theorems.ML	Tue Mar 31 22:25:46 2009 +0200
+++ b/src/HOLCF/Tools/domain/domain_theorems.ML	Tue Mar 31 15:57:10 2009 -0700
@@ -610,7 +610,7 @@
     |> (snd o PureThy.add_thmss [
         ((Binding.name "iso_rews" , iso_rews  ), [Simplifier.simp_add]),
         ((Binding.name "exhaust"  , [exhaust] ), []),
-        ((Binding.name "casedist" , [casedist]), [Induct.cases_type (Long_Name.base_name dname)]),
+        ((Binding.name "casedist" , [casedist]), [Induct.cases_type dname]),
         ((Binding.name "when_rews", when_rews ), [Simplifier.simp_add]),
         ((Binding.name "compacts", con_compacts), [Simplifier.simp_add]),
         ((Binding.name "con_rews", con_rews), [Simplifier.simp_add]),
@@ -999,6 +999,9 @@
     in pg [] goal (K tacs) end;
 end; (* local *)
 
+val inducts = ProjectRule.projections (ProofContext.init thy) ind;
+fun ind_rule (dname, rule) = ((Binding.empty, [rule]), [Induct.induct_type dname]);
+
 in thy |> Sign.add_path comp_dnam
        |> (snd o (PureThy.add_thmss (map (Thm.no_attributes o apfst Binding.name) [
 		("take_rews"  , take_rews  ),
@@ -1007,6 +1010,7 @@
 		("finite_ind", [finite_ind]),
 		("ind"       , [ind       ]),
 		("coind"     , [coind     ])])))
+       |> (snd o (PureThy.add_thmss (map ind_rule (dnames ~~ inducts))))
        |> Sign.parent_path |> pair take_rews
 end; (* let *)
 end; (* local *)