made 'lifting' plugin more robust

--- a/src/HOL/Tools/Lifting/lifting_bnf.ML	Mon Sep 08 23:09:24 2014 +0200
+++ b/src/HOL/Tools/Lifting/lifting_bnf.ML	Mon Sep 08 23:09:25 2014 +0200
@@ -95,6 +95,7 @@
   in
     [((Binding.empty, []), [([relator_eq_onp_thm], @{attributes [relator_eq_onp]})])]    
   end
+  handle ERROR _ => [] (* the "lifting" plugin should work even if "quotient" is disabled *)
 
 (* relator_mono  *)
 
@@ -112,10 +113,10 @@
   if dead_of_bnf bnf > 0 then lthy
   else
     let
-      val notes = relator_eq_onp bnf lthy @ Quotient_map bnf lthy @ relator_mono bnf
-        @ relator_distr bnf
+      val notess = [relator_eq_onp bnf lthy, Quotient_map bnf lthy, relator_mono bnf,
+        relator_distr bnf]
     in
-      snd (Local_Theory.notes notes lthy)
+      lthy |> fold (perhaps o try o (snd oo Local_Theory.notes)) notess
     end
 
 val _ = Theory.setup (bnf_interpretation lifting_plugin