--- a/src/HOL/Nominal/nominal_primrec.ML Fri Nov 13 19:57:46 2009 +0100
+++ b/src/HOL/Nominal/nominal_primrec.ML Fri Nov 13 20:41:29 2009 +0100
@@ -367,11 +367,10 @@
(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 LocalTheory.note (names_atts' ~~ map single simps) lthy';
in
lthy''
- |> LocalTheory.note "" ((qualify (Binding.name "simps"),
+ |> LocalTheory.note ((qualify (Binding.name "simps"),
map (Attrib.internal o K) [Simplifier.simp_add, Nitpick_Simps.add]),
maps snd simps')
|> snd