diff -r 2f3a2d9054d1 -r b0ea0e55dfe8 Datatype.ML
--- a/Datatype.ML	Mon Jun 20 12:05:03 1994 +0200
+++ b/Datatype.ML	Mon Jun 20 14:52:40 1994 +0200
@@ -75,7 +75,7 @@
          (if length cons < dtK then 
            "  in ineq' @ (map (fn t => sym COMP (t RS contrapos)) ineq') end"
           else "") ^ ";\n\
-       \  val induct = get_axiom thy \"induct\";\n\
+       \  val induct = get_axiom thy \"" ^ tname ^ "_induct\";\n\
        \  val cases = map (get_axiom thy) " ^
          mk_list (map (fn (s,_) => quote (tname ^ "_case_" ^ rem_quotes s)) 
                       cons) ^ ";\n\
@@ -375,7 +375,7 @@
       val Ci_neg2 =
         let val ord_t = tname ^ "_ord";
         in (Ci_neg2equals (ord_t, cons_list, 0)) @
-           [(ord_t^"0",
+           [(ord_t ^ "0",
             "(" ^ ord_t ^ "(x) ~= " ^ ord_t ^ "(y)) ==> (x ~= y)")]
         end;
 
@@ -384,9 +384,9 @@
 
       val rules_inject = Ci_ing cons_list;
 
-      val rule_induct = ("induct", t_induct cons_list tname);
+      val rule_induct = (tname ^ "_induct", t_induct cons_list tname);
 
-      val rules =rule_induct :: (rules_inject @ rules_ineq @ rules_case);
+      val rules = rule_induct :: (rules_inject @ rules_ineq @ rules_case);
   in thy
      |> add_types types
      |> add_arities arities