# HG changeset patch
# User blanchet
# Date 1410210565 -7200
# Node ID 3aa25f39cd744a3f477de47d7e9f5943629f9639
# Parent  3fb224b61995b7fb21919d1ceb8942eb8a2e90e2
made 'lifting' plugin more robust

diff -r 3fb224b61995 -r 3aa25f39cd74 src/HOL/Tools/Lifting/lifting_bnf.ML
--- 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