# HG changeset patch
# User blanchet
# Date 1382339645 -7200
# Node ID c1daa6e055656c798e8d43df19eac5350f2e38a5
# Parent  d6dc359426b7f48131c80629db552f9e90d7c144
warn about incompatible recursor signature

diff -r d6dc359426b7 -r c1daa6e05565 src/HOL/BNF/Tools/bnf_lfp_compat.ML
--- a/src/HOL/BNF/Tools/bnf_lfp_compat.ML	Mon Oct 21 08:27:51 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_lfp_compat.ML	Mon Oct 21 09:14:05 2013 +0200
@@ -57,8 +57,10 @@
     val fpTs as fpT1 :: _ = map (fn s => Type (s, As)) fpT_names';
 
     fun add_nested_types_of (T as Type (s, _)) seen =
-      if member (op =) seen T orelse s = @{type_name fun} then
+      if member (op =) seen T then
         seen
+      else if s = @{type_name fun} then
+        (warning "Partial support for recursion through functions -- 'primrec' will fail"; seen)
       else
         (case try lfp_sugar_of s of
           SOME ({T = T0, fp_res = {Ts = mutual_Ts0, ...}, ctr_sugars, ...}) =>