--- 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