Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
robustness
authorblanchet
Mon, 24 Oct 2016 20:32:02 +0200
changeset 64381 59f59f826afd
parent 64380 4b22e1268779
child 64382 2a75139b5931
robustness
src/HOL/Tools/BNF/bnf_gfp_grec_sugar.ML file | annotate | diff | comparison | revisions 
--- 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;
isabelle