src/HOL/Nominal/nominal_primrec.ML
changeset 33766 c679f05600cd
parent 33726 0878aecbf119
child 33968 f94fb13ecbb3
     1.1 --- a/src/HOL/Nominal/nominal_primrec.ML	Thu Nov 19 14:45:56 2009 +0100
     1.2 +++ b/src/HOL/Nominal/nominal_primrec.ML	Thu Nov 19 14:46:33 2009 +0100
     1.3 @@ -280,7 +280,7 @@
     1.4        else primrec_err ("functions " ^ commas_quote names2 ^
     1.5          "\nare not mutually recursive");
     1.6      val (defs_thms, lthy') = lthy |>
     1.7 -      fold_map (apfst (snd o snd) oo Local_Theory.define Thm.definitionK o fst) defs';
     1.8 +      fold_map (apfst (snd o snd) oo Local_Theory.define o fst) defs';
     1.9      val qualify = Binding.qualify false
    1.10        (space_implode "_" (map (Long_Name.base_name o #1) defs));
    1.11      val names_atts' = map (apfst qualify) names_atts;