Fixed bug in add_datatype_axm:
authorberghofe
Fri Mar 05 12:11:54 1999 +0100 (1999-03-05)
changeset 63054cbdb974220c
parent 6304 9a82e1c3d9da
child 6306 81e7fbf61db2
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.
src/HOL/Tools/datatype_package.ML
     1.1 --- a/src/HOL/Tools/datatype_package.ML	Thu Mar 04 14:23:51 1999 +0100
     1.2 +++ b/src/HOL/Tools/datatype_package.ML	Fri Mar 05 12:11:54 1999 +0100
     1.3 @@ -299,7 +299,7 @@
     1.4  
     1.5      val case_names = map (fn s => (s ^ "_case")) new_type_names;
     1.6  
     1.7 -    val thy2 = thy |>
     1.8 +    val thy2' = thy |>
     1.9  
    1.10        (** new types **)
    1.11  
    1.12 @@ -323,7 +323,12 @@
    1.13        Theory.add_consts_i (map (fn ((name, T), Ts) =>
    1.14          (name, Ts @ [T] ---> freeT, NoSyn))
    1.15            (case_names ~~ newTs ~~ case_fn_Ts)) |>
    1.16 -      Theory.add_trrules_i (DatatypeProp.make_case_trrules new_type_names descr) |>
    1.17 +      Theory.add_trrules_i (DatatypeProp.make_case_trrules new_type_names descr);
    1.18 +
    1.19 +    val reccomb_names' = map (Sign.intern_const (sign_of thy2')) reccomb_names;
    1.20 +    val case_names' = map (Sign.intern_const (sign_of thy2')) case_names;
    1.21 +
    1.22 +    val thy2 = thy2' |>
    1.23  
    1.24        (** t_ord functions **)
    1.25  
    1.26 @@ -383,8 +388,8 @@
    1.27      val (thy10, case_congs) = add_and_get_axioms "case_cong" new_type_names
    1.28        (DatatypeProp.make_case_congs new_type_names descr sorts thy9) thy9;
    1.29      
    1.30 -    val dt_infos = map (make_dt_info descr' induct reccomb_names rec_thms)
    1.31 -      ((0 upto length (hd descr) - 1) ~~ (hd descr) ~~ case_names ~~ case_thms ~~
    1.32 +    val dt_infos = map (make_dt_info descr' induct reccomb_names' rec_thms)
    1.33 +      ((0 upto length (hd descr) - 1) ~~ (hd descr) ~~ case_names' ~~ case_thms ~~
    1.34          exhaustion ~~ distinct ~~ inject ~~ nchotomys ~~ case_congs);
    1.35  
    1.36      val simps = flat (distinct @ inject @ case_thms) @ size_thms @ rec_thms;