# HG changeset patch
# User blanchet
# Date 1425553054 -3600
# Node ID 70a68edcc79b9f3fd87eac3d492b2d1d775f25a3
# Parent  c067eba942e7c7e8d00ac88fb363e326038938e0
helpful error message when 'auto' fails

diff -r c067eba942e7 -r 70a68edcc79b src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML
--- a/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML	Thu Mar 05 11:57:34 2015 +0100
+++ b/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML	Thu Mar 05 11:57:34 2015 +0100
@@ -92,6 +92,8 @@
   error_at ctxt [t] "Invalid map function";
 fun unexpected_corec_call ctxt eqns t =
   error_at ctxt eqns ("Unexpected corecursive call in " ^ quote (Syntax.string_of_term ctxt t));
+fun use_primcorecursive () =
+  error "\"auto\" failed (try \"primcorecursive\" instead of \"primcorec\")";
 
 datatype corec_option =
   Plugins_Option of Proof.context -> Plugin_Name.filter |
@@ -1073,9 +1075,10 @@
         tac_opt;
 
     val excludess'' = @{map 3} (fn tac_opt => fn sequential => map (fn (j, goal) =>
-        (j, (Option.map (Goal.prove (*no sorry*) lthy [] [] goal #> Thm.close_derivation)
-           (exclude_tac tac_opt sequential j), goal))))
-      tac_opts sequentials excludess';
+          (j, (Option.map (Goal.prove (*no sorry*) lthy [] [] goal #> Thm.close_derivation)
+             (exclude_tac tac_opt sequential j), goal))))
+        tac_opts sequentials excludess'
+      handle ERROR _ => use_primcorecursive ();
 
     val taut_thmss = map (map (apsnd (the o fst)) o filter (is_some o fst o snd)) excludess'';
     val (goal_idxss, exclude_goalss) = excludess''
@@ -1109,6 +1112,7 @@
                 [Goal.prove (*no sorry*) lthy [] [] goal (fn {context = ctxt, ...} =>
                    mk_primcorec_nchotomy_tac ctxt (res_exhaust_discs @ arg_exhaust_discs))
                  |> Thm.close_derivation]
+                handle ERROR _ => use_primcorecursive ()
               end
             | false =>
               (case tac_opt of
@@ -1480,10 +1484,8 @@
   |> Seq.hd) ooo add_primcorec_ursive_cmd false;
 
 val add_primcorec_cmd = (fn (goalss, after_qed, lthy) =>
-  lthy
-  |> after_qed (map (fn [] => []
-      | _ => error "\"auto\" failed -- use \"primcorecursive\" instead of \"primcorec\"")
-    goalss)) ooo add_primcorec_ursive_cmd true;
+    lthy |> after_qed (map (fn [] => [] | _ => use_primcorecursive ()) goalss)) ooo
+  add_primcorec_ursive_cmd true;
 
 val corec_option_parser = Parse.group (K "option")
   (Plugin_Name.parse_filter >> Plugins_Option