author | blanchet |
Mon, 24 Oct 2016 20:32:02 +0200 | |
changeset 64381 | 59f59f826afd |
parent 64380 | 4b22e1268779 |
child 64382 | 2a75139b5931 |
--- 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;