[isabelle-dev] "local_setup" and "Generic_Data"

Jasmin Blanchette jasmin.blanchette at gmail.com
Fri Aug 6 16:56:26 CEST 2010

Hi all,

I was trying to make Nitpick more context-friendly and thought that "local_setup" and "Generic_Data" would be my friends. However, "local_setup" seems to do nothing -- the changes I perform to the data are coldly ignored. The little theory below shows illustrates what I mean:

theory Scratch
imports Main

ML {*
structure Data = Generic_Data(
  type T = int
  val empty = 0
  val extend = I
  val merge = Int.max)

setup {* Context.theory_map (Data.map (Integer.add 1)) *}
ML {* Data.get (Context.Theory @{theory}) *}  (* OK: returns 1 *)

locale x =
  fixes R :: 'a

local_setup {* Context.proof_map (Data.map (Integer.add 3)) *}
ML {* Data.get (Context.Theory @{theory}) *}  (* OK: returns 1 *)
ML {* Data.get (Context.Proof @{context}) *}  (* Not OK: returns 1, expected 4 *)


I reproduced this behavior with both Isabelle2009-1 (where "local_setup" was introduced) and a recent repository version.
Does anybody knows what's going on?



More information about the isabelle-dev mailing list