# HG changeset patch
# User blanchet
# Date 1464688485 -7200
# Node ID d5974697765bb20fcfb4c6b167988748b03f046e
# Parent  38d6aabec460bc42dec682a676f47df3df777e76
made parsing of monomorphic/polymorphic constants more robust

diff -r 38d6aabec460 -r d5974697765b src/HOL/Tools/BNF/bnf_gfp_grec_sugar.ML
--- a/src/HOL/Tools/BNF/bnf_gfp_grec_sugar.ML	Tue May 31 10:53:11 2016 +0200
+++ b/src/HOL/Tools/BNF/bnf_gfp_grec_sugar.ML	Tue May 31 11:54:45 2016 +0200
@@ -1436,14 +1436,26 @@
                   let
                     val arg_ts' = map fst exp_arg_ts;
                     val fun_t' = Const (s, fun_U);
-                    val t' = build_function_after_encapsulation fun_t fun_t' params arg_ts arg_ts';
+
+                    fun finish_off () =
+                      let
+                        val t' =
+                          build_function_after_encapsulation fun_t fun_t' params arg_ts arg_ts';
+                      in
+                        if can type_of1 (bound_Us, t') then
+                          (if fun_T = fun_U orelse is_special_parametric_const (s, fun_T) then ()
+                           else add_parametric_const s general_T fun_T fun_U;
+                           t')
+                        else
+                          explore params t
+                      end;
                   in
-                    if can type_of1 (bound_Us, t') then
-                      (if fun_T = fun_U orelse is_special_parametric_const (s, fun_T) then ()
-                       else add_parametric_const s general_T fun_T fun_U;
-                       t')
+                    if polymorphic then
+                      finish_off ()
                     else
-                      explore params t
+                      (case try finish_off () of
+                        SOME t' => t'
+                      | NONE => explore params t)
                   end
                 | NONE => explore params t)
               end