# HG changeset patch
# User blanchet
# Date 1464684790 -7200
# Node ID da1cd3ce80c24ad8e2f2b72968bac47a4b95e632
# Parent  dc221b8945f20a3948177338e22b456c783985f6
error message

diff -r dc221b8945f2 -r da1cd3ce80c2 src/HOL/Tools/BNF/bnf_gfp_grec.ML
--- a/src/HOL/Tools/BNF/bnf_gfp_grec.ML	Tue May 31 11:45:34 2016 +1000
+++ b/src/HOL/Tools/BNF/bnf_gfp_grec.ML	Tue May 31 10:53:10 2016 +0200
@@ -3045,8 +3045,11 @@
     let
       val (exprs, lthy) = nonempty_corec_info_exprs_of fpT_name lthy;
       val thy = Proof_Context.theory_of lthy;
-      val SOME expr =
-        find_first ((fn {fpT, ...} => Sign.typ_instance thy (res_T, fpT)) o corec_ad_of_expr) exprs;
+      val expr =
+        (case find_first ((fn {fpT, ...} => Sign.typ_instance thy (res_T, fpT)) o corec_ad_of_expr)
+            exprs of
+          SOME expr => expr
+        | NONE => error ("Invalid type: " ^ Syntax.string_of_typ lthy res_T));
       val (info, lthy) = corec_info_of_expr expr lthy;
     in
       (instantiate_corec_info thy res_T info, lthy |> is_Ad expr ? register_corec_info info)