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.
warn about incompatible recursor signature
authorblanchet
Mon, 21 Oct 2013 09:14:05 +0200
changeset 54179 c1daa6e05565
parent 54178 d6dc359426b7
child 54180 1753c57eb16c
warn about incompatible recursor signature
src/HOL/BNF/Tools/bnf_lfp_compat.ML file | annotate | diff | comparison | revisions 
--- 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, ...}) =>
isabelle