adding ROOT.ML to HOL-Mutabelle session; uncommenting HOL.induct constants in Mutabelle session

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Mutabelle/ROOT.ML	Tue Feb 23 13:57:51 2010 +0100
@@ -0,0 +1,3 @@
+
+use_thy "MutabelleExtra";
+

--- a/src/HOL/Mutabelle/mutabelle_extra.ML	Tue Feb 23 13:36:15 2010 +0100
+++ b/src/HOL/Mutabelle/mutabelle_extra.ML	Tue Feb 23 13:57:51 2010 +0100
@@ -192,9 +192,9 @@
 
 val forbidden =
  [(* (@{const_name "power"}, "'a"), *)
-  (@{const_name HOL.induct_equal}, "'a"),
-  (@{const_name HOL.induct_implies}, "'a"),
-  (@{const_name HOL.induct_conj}, "'a"),
+  (*(@{const_name induct_equal}, "'a"),
+  (@{const_name induct_implies}, "'a"),
+  (@{const_name induct_conj}, "'a"),*)
   (@{const_name "undefined"}, "'a"),
   (@{const_name "default"}, "'a"),
   (@{const_name "dummy_pattern"}, "'a::{}") (*,