src/HOL/Nominal/nominal_primrec.ML
changeset 30280 eb98b49ef835
parent 30253 63cae7fd7e64
child 30364 577edc39b501
     1.1 --- a/src/HOL/Nominal/nominal_primrec.ML	Thu Mar 05 11:58:53 2009 +0100
     1.2 +++ b/src/HOL/Nominal/nominal_primrec.ML	Thu Mar 05 12:08:00 2009 +0100
     1.3 @@ -207,7 +207,7 @@
     1.4      val frees = ls @ x :: rs;
     1.5      val raw_rhs = list_abs_free (frees,
     1.6        list_comb (Const (rec_name, dummyT), fs @ [Free x]))
     1.7 -    val def_name = Thm.def_name (Sign.base_name fname);
     1.8 +    val def_name = Thm.def_name (NameSpace.base_name fname);
     1.9      val rhs = singleton (Syntax.check_terms ctxt) raw_rhs;
    1.10      val SOME var = get_first (fn ((b, _), mx) =>
    1.11        if Binding.name_of b = fname then SOME (b, mx) else NONE) fixes;
    1.12 @@ -286,7 +286,7 @@
    1.13        fold_map (apfst (snd o snd) oo
    1.14          LocalTheory.define Thm.definitionK o fst) defs';
    1.15      val qualify = Binding.qualify false
    1.16 -      (space_implode "_" (map (Sign.base_name o #1) defs));
    1.17 +      (space_implode "_" (map (NameSpace.base_name o #1) defs));
    1.18      val names_atts' = map (apfst qualify) names_atts;
    1.19      val cert = cterm_of (ProofContext.theory_of lthy');
    1.20