# HG changeset patch
# User blanchet
# Date 1456498175 -3600
# Node ID 6dce7bf7960becde9cb44ef3b5c109d26da16f21
# Parent  bd650e3a210f62a1041e3be7fc1345db3643a5c8
generalized ML function

diff -r bd650e3a210f -r 6dce7bf7960b src/HOL/Tools/BNF/bnf_def.ML
--- a/src/HOL/Tools/BNF/bnf_def.ML	Fri Feb 26 15:00:47 2016 +0100
+++ b/src/HOL/Tools/BNF/bnf_def.ML	Fri Feb 26 15:49:35 2016 +0100
@@ -743,13 +743,19 @@
           (Type (s, Ts), Type (s', Us)) =>
           if s = s' then
             let
-              val (live, cst0) =
-                (case AList.lookup (op =) pre_cst_table s of
-                  NONE => let val bnf = the (bnf_of ctxt s) in (live_of_bnf bnf, of_bnf bnf) end
-                | SOME p => p);
-              val cst = mk live Ts Us cst0;
-              val TUs' = map dest (fst (strip_typeN live (fastype_of cst)));
-            in Term.list_comb (cst, map build TUs') end
+              fun recurse (live, cst0) =
+                let
+                  val cst = mk live Ts Us cst0;
+                  val TUs' = map dest (fst (strip_typeN live (fastype_of cst)));
+                in Term.list_comb (cst, map build TUs') end;
+            in
+              (case AList.lookup (op =) pre_cst_table s of
+                NONE =>
+                (case bnf_of ctxt s of
+                  SOME bnf => recurse (live_of_bnf bnf, of_bnf bnf)
+                | NONE => build_simple TU)
+              | SOME entry => recurse entry)
+            end
           else
             build_simple TU
         | _ => build_simple TU);