# HG changeset patch
# User blanchet
# Date 1425553054 -3600
# Node ID c067eba942e7c7e8d00ac88fb363e326038938e0
# Parent  2d90b85b92649885c5f771ef7b22ba11aea6e6f2
no quick_and_dirty for goals that may fail + tuned messages

diff -r 2d90b85b9264 -r c067eba942e7 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
@@ -91,7 +91,7 @@
 fun invalid_map ctxt t =
   error_at ctxt [t] "Invalid map function";
 fun unexpected_corec_call ctxt eqns t =
-  error_at ctxt eqns ("Unexpected corecursive call " ^ quote (Syntax.string_of_term ctxt t));
+  error_at ctxt eqns ("Unexpected corecursive call in " ^ quote (Syntax.string_of_term ctxt t));
 
 datatype corec_option =
   Plugins_Option of Proof.context -> Plugin_Name.filter |
@@ -217,11 +217,11 @@
     SOME {casex = Const (s', _), split_sels = _ :: _, ...} => SOME s'
   | _ => NONE);
 
-fun massage_let_if_case ctxt has_call massage_leaf =
+fun massage_let_if_case ctxt has_call massage_leaf bound_Ts t0 =
   let
     val thy = Proof_Context.theory_of ctxt;
 
-    fun check_no_call t = if has_call t then unexpected_corec_call ctxt [] t else ();
+    fun check_no_call t = if has_call t then unexpected_corec_call ctxt [t0] t else ();
 
     fun massage_abs bound_Ts 0 t = massage_rec bound_Ts t
       | massage_abs bound_Ts m (Abs (s, T, t)) = Abs (s, T, massage_abs (T :: bound_Ts) (m - 1) t)
@@ -271,14 +271,14 @@
         | _ => massage_leaf bound_Ts t)
       end;
   in
-    massage_rec
+    massage_rec bound_Ts t0
   end;
 
 fun curried_type (Type (@{type_name fun}, [Type (@{type_name prod}, Ts), T])) = Ts ---> T;
 
-fun massage_nested_corec_call ctxt has_call raw_massage_call bound_Ts U t =
+fun massage_nested_corec_call ctxt has_call raw_massage_call bound_Ts U t0 =
   let
-    fun check_no_call t = if has_call t then unexpected_corec_call ctxt [] t else ();
+    fun check_no_call t = if has_call t then unexpected_corec_call ctxt [t0] t else ();
 
     val build_map_Inl = build_map ctxt [] (uncurry Inl_const o dest_sumT o snd);
 
@@ -357,9 +357,9 @@
         else
           build_map_Inl (T, U) $ t) bound_Ts;
 
-    val T = fastype_of1 (bound_Ts, t);
+    val T = fastype_of1 (bound_Ts, t0);
   in
-    if has_call t then massage_call bound_Ts U T t else build_map_Inl (T, U) $ t
+    if has_call t0 then massage_call bound_Ts U T t0 else build_map_Inl (T, U) $ t0
   end;
 
 fun expand_to_ctr_term ctxt s Ts t =
@@ -1073,7 +1073,7 @@
         tac_opt;
 
     val excludess'' = @{map 3} (fn tac_opt => fn sequential => map (fn (j, goal) =>
-        (j, (Option.map (Goal.prove_sorry lthy [] [] goal #> Thm.close_derivation)
+        (j, (Option.map (Goal.prove (*no sorry*) lthy [] [] goal #> Thm.close_derivation)
            (exclude_tac tac_opt sequential j), goal))))
       tac_opts sequentials excludess';
 
@@ -1106,7 +1106,7 @@
                 val (_, _, arg_exhaust_discs, _, _) =
                   case_thms_of_term lthy (the_default Term.dummy code_rhs_opt);
               in
-                [Goal.prove_sorry lthy [] [] goal (fn {context = ctxt, ...} =>
+                [Goal.prove (*no sorry*) lthy [] [] goal (fn {context = ctxt, ...} =>
                    mk_primcorec_nchotomy_tac ctxt (res_exhaust_discs @ arg_exhaust_discs))
                  |> Thm.close_derivation]
               end