[isabelle] Interpreting a locale leaving some parameters unfixed



Hi all,
  consider the following boiled down example, where I try to interpret a
  locale while leaving some (all) parameters unspecified.


locale foo = fixes x::nat begin
  definition "c = x + x"
end

interpretation foo .
*** Illegal free variable(s) in term: x
in constant abbreviation "c"


Why do I get this error message, and can I somehow work around it?
I would have expected an abbreviation of the form "c x == foo.c x" to be
declared.


In my concrete use-case, the locales have no assumptions, and I have to
instantiate some parameters.

--
  Peter






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