src/HOL/Tools/inductive_set_package.ML
changeset 29006 abe0f11cfa4e
parent 28965 1de908189869
child 29064 70a61d58460e
     1.1 --- a/src/HOL/Tools/inductive_set_package.ML	Fri Dec 05 18:42:39 2008 +0100
     1.2 +++ b/src/HOL/Tools/inductive_set_package.ML	Fri Dec 05 18:43:42 2008 +0100
     1.3 @@ -499,9 +499,9 @@
     1.4      (* convert theorems to set notation *)
     1.5      val rec_name =
     1.6        if Binding.is_empty alt_name then
     1.7 -        Binding.name (space_implode "_" (map (Name.name_of o fst) cnames_syn))
     1.8 +        Binding.name (space_implode "_" (map (Binding.base_name o fst) cnames_syn))
     1.9        else alt_name;
    1.10 -    val cnames = map (Sign.full_bname (ProofContext.theory_of ctxt3) o Name.name_of o #1) cnames_syn;  (* FIXME *)
    1.11 +    val cnames = map (Sign.full_name (ProofContext.theory_of ctxt3) o #1) cnames_syn;  (* FIXME *)
    1.12      val (intr_names, intr_atts) = split_list (map fst intros);
    1.13      val raw_induct' = to_set [] (Context.Proof ctxt3) raw_induct;
    1.14      val (intrs', elims', induct, ctxt4) =