# HG changeset patch
# User berghofe
# Date 920632314 -3600
# Node ID 4cbdb974220c6ce44850ba0c3522c49c4e7659f9
# Parent  9a82e1c3d9da002fab244372969a92fb7f928311
Fixed bug in add_datatype_axm:
Recursion and case combinators were assigned inconsistent names in
quick_and_dirty mode, which caused recdef etc. to crash.

diff -r 9a82e1c3d9da -r 4cbdb974220c src/HOL/Tools/datatype_package.ML
--- a/src/HOL/Tools/datatype_package.ML	Thu Mar 04 14:23:51 1999 +0100
+++ b/src/HOL/Tools/datatype_package.ML	Fri Mar 05 12:11:54 1999 +0100
@@ -299,7 +299,7 @@
 
     val case_names = map (fn s => (s ^ "_case")) new_type_names;
 
-    val thy2 = thy |>
+    val thy2' = thy |>
 
       (** new types **)
 
@@ -323,7 +323,12 @@
       Theory.add_consts_i (map (fn ((name, T), Ts) =>
         (name, Ts @ [T] ---> freeT, NoSyn))
           (case_names ~~ newTs ~~ case_fn_Ts)) |>
-      Theory.add_trrules_i (DatatypeProp.make_case_trrules new_type_names descr) |>
+      Theory.add_trrules_i (DatatypeProp.make_case_trrules new_type_names descr);
+
+    val reccomb_names' = map (Sign.intern_const (sign_of thy2')) reccomb_names;
+    val case_names' = map (Sign.intern_const (sign_of thy2')) case_names;
+
+    val thy2 = thy2' |>
 
       (** t_ord functions **)
 
@@ -383,8 +388,8 @@
     val (thy10, case_congs) = add_and_get_axioms "case_cong" new_type_names
       (DatatypeProp.make_case_congs new_type_names descr sorts thy9) thy9;
     
-    val dt_infos = map (make_dt_info descr' induct reccomb_names rec_thms)
-      ((0 upto length (hd descr) - 1) ~~ (hd descr) ~~ case_names ~~ case_thms ~~
+    val dt_infos = map (make_dt_info descr' induct reccomb_names' rec_thms)
+      ((0 upto length (hd descr) - 1) ~~ (hd descr) ~~ case_names' ~~ case_thms ~~
         exhaustion ~~ distinct ~~ inject ~~ nchotomys ~~ case_congs);
 
     val simps = flat (distinct @ inject @ case_thms) @ size_thms @ rec_thms;