--- a/src/HOL/Nominal/nominal_primrec.ML Fri Nov 13 20:41:29 2009 +0100
+++ b/src/HOL/Nominal/nominal_primrec.ML Fri Nov 13 21:11:15 2009 +0100
@@ -280,9 +280,8 @@
else primrec_err ("functions " ^ commas_quote names2 ^
"\nare not mutually recursive");
val (defs_thms, lthy') = lthy |>
- set_group ? LocalTheory.set_group (serial ()) |>
- fold_map (apfst (snd o snd) oo
- LocalTheory.define Thm.definitionK o fst) defs';
+ set_group ? Local_Theory.set_group (serial ()) |>
+ fold_map (apfst (snd o snd) oo Local_Theory.define Thm.definitionK o fst) defs';
val qualify = Binding.qualify false
(space_implode "_" (map (Long_Name.base_name o #1) defs));
val names_atts' = map (apfst qualify) names_atts;
@@ -367,10 +366,11 @@
(fn thss => fn goal_ctxt =>
let
val simps = ProofContext.export goal_ctxt lthy' (flat thss);
- val (simps', lthy'') = fold_map LocalTheory.note (names_atts' ~~ map single simps) lthy';
+ val (simps', lthy'') =
+ fold_map Local_Theory.note (names_atts' ~~ map single simps) lthy';
in
lthy''
- |> LocalTheory.note ((qualify (Binding.name "simps"),
+ |> Local_Theory.note ((qualify (Binding.name "simps"),
map (Attrib.internal o K) [Simplifier.simp_add, Nitpick_Simps.add]),
maps snd simps')
|> snd