[isabelle] baffled by fun error message

Hello mailing-list!

When I try the following minimal example in Isabelle2015

theory Test
imports Main

datatype (funs : 'f, 'v) "term" = Var 'v | Fun 'f "('f, 'v) term list"

type_synonym ('f, 'v) trs = "(('f, 'v) term à ('f, 'v) term) set"

  fixes F and R :: "('f, 'v) trs"
  assumes "R â F"

fun star :: "('f, 'v) term â ('f, 'v) term"
  "star (Fun f ts) = Fun f (map star ts)"



I get the error message:

exception THM 0 raised (line 744 of "thm.ML"):
  forall_intr: variable "R" free in assumptions
  wf R â
  (âf ts x. x â set ts â (x, Fun f ts) â R) â
  âx. Wellfounded.accp star_rel x
    [star_rel â ??.Test.star_rel]

Which leaves me quite puzzled. I do neither understand the error
message nor why there is an error at all. Can somebody explain what
happens here, please?

Cheers, Thomas

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.