src/HOL/Nominal/nominal_primrec.ML
changeset 33671 4b0f2599ed48
parent 33670 02b7738aef6a
child 33726 0878aecbf119
     1.1 --- a/src/HOL/Nominal/nominal_primrec.ML	Fri Nov 13 20:41:29 2009 +0100
     1.2 +++ b/src/HOL/Nominal/nominal_primrec.ML	Fri Nov 13 21:11:15 2009 +0100
     1.3 @@ -280,9 +280,8 @@
     1.4        else primrec_err ("functions " ^ commas_quote names2 ^
     1.5          "\nare not mutually recursive");
     1.6      val (defs_thms, lthy') = lthy |>
     1.7 -      set_group ? LocalTheory.set_group (serial ()) |>
     1.8 -      fold_map (apfst (snd o snd) oo
     1.9 -        LocalTheory.define Thm.definitionK o fst) defs';
    1.10 +      set_group ? Local_Theory.set_group (serial ()) |>
    1.11 +      fold_map (apfst (snd o snd) oo Local_Theory.define Thm.definitionK o fst) defs';
    1.12      val qualify = Binding.qualify false
    1.13        (space_implode "_" (map (Long_Name.base_name o #1) defs));
    1.14      val names_atts' = map (apfst qualify) names_atts;
    1.15 @@ -367,10 +366,11 @@
    1.16        (fn thss => fn goal_ctxt =>
    1.17           let
    1.18             val simps = ProofContext.export goal_ctxt lthy' (flat thss);
    1.19 -           val (simps', lthy'') = fold_map LocalTheory.note (names_atts' ~~ map single simps) lthy';
    1.20 +           val (simps', lthy'') =
    1.21 +            fold_map Local_Theory.note (names_atts' ~~ map single simps) lthy';
    1.22           in
    1.23             lthy''
    1.24 -           |> LocalTheory.note ((qualify (Binding.name "simps"),
    1.25 +           |> Local_Theory.note ((qualify (Binding.name "simps"),
    1.26                  map (Attrib.internal o K) [Simplifier.simp_add, Nitpick_Simps.add]),
    1.27                  maps snd simps')
    1.28             |> snd