Fixed bug in mk_ind_def that caused the inductive definition package to
authorberghofe
Wed Oct 15 11:02:28 2003 +0200 (2003-10-15 ago)
changeset 14235281295a1bbaa
parent 14234 9590df3c5f2a
child 14236 c73d62ce9d1c
Fixed bug in mk_ind_def that caused the inductive definition package to
crash in cases where the declaration of a constant and its definition
were located in different theory files.
src/HOL/Tools/inductive_package.ML
     1.1 --- a/src/HOL/Tools/inductive_package.ML	Wed Oct 15 07:03:43 2003 +0200
     1.2 +++ b/src/HOL/Tools/inductive_package.ML	Wed Oct 15 11:02:28 2003 +0200
     1.3 @@ -697,7 +697,7 @@
     1.4  
     1.5  fun cond_declare_consts declare_consts cs paramTs cnames =
     1.6    if declare_consts then
     1.7 -    Theory.add_consts_i (map (fn (c, n) => (n, paramTs ---> fastype_of c, NoSyn)) (cs ~~ cnames))
     1.8 +    Theory.add_consts_i (map (fn (c, n) => (Sign.base_name n, paramTs ---> fastype_of c, NoSyn)) (cs ~~ cnames))
     1.9    else I;
    1.10  
    1.11  fun mk_ind_def declare_consts alt_name coind cs intr_ts monos thy
    1.12 @@ -738,8 +738,10 @@
    1.13  
    1.14      (* add definiton of recursive sets to theory *)
    1.15  
    1.16 -    val rec_name = if alt_name = "" then space_implode "_" cnames else alt_name;
    1.17 -    val full_rec_name = Sign.full_name (Theory.sign_of thy) rec_name;
    1.18 +    val rec_name = if alt_name = "" then
    1.19 +      space_implode "_" (map Sign.base_name cnames) else alt_name;
    1.20 +    val full_rec_name = if length cs < 2 then hd cnames
    1.21 +      else Sign.full_name (Theory.sign_of thy) rec_name;
    1.22  
    1.23      val rec_const = list_comb
    1.24        (Const (full_rec_name, paramTs ---> setT), params);
    1.25 @@ -767,7 +769,7 @@
    1.26    let
    1.27      val _ =
    1.28        if verbose then message ("Proofs for " ^ coind_prefix coind ^ "inductive set(s) " ^
    1.29 -        commas_quote cnames) else ();
    1.30 +        commas_quote (map Sign.base_name cnames)) else ();
    1.31  
    1.32      val ((intr_names, intr_ts), intr_atts) = apfst split_list (split_list intros);
    1.33  
    1.34 @@ -832,9 +834,8 @@
    1.35      val cTs = map (try_term (HOLogic.dest_setT o fastype_of)
    1.36        "Recursive component not of type set: " sign) cs;
    1.37  
    1.38 -    val full_cnames = map (try_term (fst o dest_Const o head_of)
    1.39 +    val cnames = map (try_term (fst o dest_Const o head_of)
    1.40        "Recursive set not previously declared as constant: " sign) cs;
    1.41 -    val cnames = map Sign.base_name full_cnames;
    1.42  
    1.43      val save_sign =
    1.44        thy |> Theory.copy |> cond_declare_consts declare_consts cs paramTs cnames |> Theory.sign_of;
    1.45 @@ -845,9 +846,9 @@
    1.46        add_ind_def verbose declare_consts alt_name coind no_elim no_ind cs intros monos
    1.47          thy params paramTs cTs cnames induct_cases;
    1.48      val thy2 = thy1
    1.49 -      |> put_inductives full_cnames ({names = full_cnames, coind = coind}, result)
    1.50 +      |> put_inductives cnames ({names = cnames, coind = coind}, result)
    1.51        |> add_cases_induct no_elim (no_ind orelse coind orelse length cs > 1)
    1.52 -          full_cnames elims induct;
    1.53 +          cnames elims induct;
    1.54    in (thy2, result) end;
    1.55  
    1.56  fun add_inductive verbose coind c_strings intro_srcs raw_monos thy =