# HG changeset patch
# User blanchet
# Date 1477333922 -7200
# Node ID 59f59f826afd4354aa6cc173eac1e1ae6f4f2100
# Parent  4b22e1268779d4ebbd25d9ecf84da75567f46084
robustness

diff -r 4b22e1268779 -r 59f59f826afd src/HOL/Tools/BNF/bnf_gfp_grec_sugar.ML
--- a/src/HOL/Tools/BNF/bnf_gfp_grec_sugar.ML	Mon Oct 24 18:25:30 2016 +0200
+++ b/src/HOL/Tools/BNF/bnf_gfp_grec_sugar.ML	Mon Oct 24 20:32:02 2016 +0200
@@ -2257,7 +2257,8 @@
       |> (case raw_fun_T_opt of
            SOME raw_T =>
            Proof_Context.add_const_constraint (fun_name, SOME (Syntax.read_typ lthy raw_T))
-         | NONE => I);
+         | NONE => I)
+      handle TYPE (s, _, _) => error s;
 
     val fun_b = Binding.name (Long_Name.base_name fun_name);
     val code_goal = Syntax.read_prop fake_lthy raw_eq;