# HG changeset patch
# User blanchet
# Date 1427451646 -3600
# Node ID a03696dc3283c1d142427740d222531f294420d2
# Parent  f014a2dc0ac878cab8dab59e4156f32be9384ca8
more graceful failure if some of the involved BNFs have no data

diff -r f014a2dc0ac8 -r a03696dc3283 src/HOL/Tools/Lifting/lifting_bnf.ML
--- a/src/HOL/Tools/Lifting/lifting_bnf.ML	Fri Mar 27 09:56:34 2015 +0100
+++ b/src/HOL/Tools/Lifting/lifting_bnf.ML	Fri Mar 27 11:20:46 2015 +0100
@@ -93,7 +93,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 *)
+  handle NO_PRED_DATA _ => [] (* the "lifting" plugin should work even if "quotient" is disabled *)
 
 (* relator_mono  *)
 
diff -r f014a2dc0ac8 -r a03696dc3283 src/HOL/Tools/Transfer/transfer_bnf.ML
--- a/src/HOL/Tools/Transfer/transfer_bnf.ML	Fri Mar 27 09:56:34 2015 +0100
+++ b/src/HOL/Tools/Transfer/transfer_bnf.ML	Fri Mar 27 11:20:46 2015 +0100
@@ -6,6 +6,8 @@
 
 signature TRANSFER_BNF =
 sig
+  exception NO_PRED_DATA of unit
+
   val transfer_plugin: string
   val base_name_of_bnf: BNF_Def.bnf -> binding
   val type_name_of_bnf: BNF_Def.bnf -> string
@@ -21,6 +23,8 @@
 open BNF_FP_Util
 open BNF_FP_Def_Sugar
 
+exception NO_PRED_DATA of unit
+
 val transfer_plugin = Plugin_Name.declare_setup @{binding transfer}
 
 (* util functions *)
@@ -318,9 +322,9 @@
 (* simplification rules for the predicator *)
 
 fun lookup_defined_pred_data lthy name =
-  case (Transfer.lookup_pred_data lthy name) of
+  case Transfer.lookup_pred_data lthy name of
     SOME data => data
-    | NONE => (error "lookup_pred_data: something went utterly wrong")
+  | NONE => raise NO_PRED_DATA ()
 
 fun lives_of_fp (fp_sugar: fp_sugar) =
   let
@@ -377,6 +381,7 @@
     |> Variable.export lthy old_lthy
     |> map Drule.zero_var_indexes
   end
+  handle NO_PRED_DATA () => []
 
 
 (* fp_sugar interpretation *)