# HG changeset patch
# User wenzelm
# Date 1185712207 -7200
# Node ID 896fb015079cfc6e4153649356cccea5933dcce8
# Parent  248da5f0e735c59d7ec005ae20cde56a65dce94b
replaced program_defs_ref by proper context data (via attribute "program");

diff -r 248da5f0e735 -r 896fb015079c src/ZF/UNITY/AllocImpl.thy
--- a/src/ZF/UNITY/AllocImpl.thy	Sun Jul 29 14:30:06 2007 +0200
+++ b/src/ZF/UNITY/AllocImpl.thy	Sun Jul 29 14:30:07 2007 +0200
@@ -69,10 +69,7 @@
 
 declare alloc_prog_def [THEN def_prg_Init, simp]
 declare alloc_prog_def [THEN def_prg_AllowedActs, simp]
-ML
-{*
-program_defs_ref := [thm"alloc_prog_def"]
-*}
+declare alloc_prog_def [program]
 
 declare  alloc_giv_act_def [THEN def_act_simp, simp]
 declare  alloc_rel_act_def [THEN def_act_simp, simp]
diff -r 248da5f0e735 -r 896fb015079c src/ZF/UNITY/ClientImpl.thy
--- a/src/ZF/UNITY/ClientImpl.thy	Sun Jul 29 14:30:06 2007 +0200
+++ b/src/ZF/UNITY/ClientImpl.thy	Sun Jul 29 14:30:07 2007 +0200
@@ -96,10 +96,7 @@
 
 declare client_prog_def [THEN def_prg_Init, simp]
 declare client_prog_def [THEN def_prg_AllowedActs, simp]
-ML
-{*
-program_defs_ref := [thm"client_prog_def"]
-*}
+declare client_prog_def [program]
 
 declare  client_rel_act_def [THEN def_act_simp, simp]
 declare  client_tok_act_def [THEN def_act_simp, simp]
diff -r 248da5f0e735 -r 896fb015079c src/ZF/UNITY/Constrains.thy
--- a/src/ZF/UNITY/Constrains.thy	Sun Jul 29 14:30:06 2007 +0200
+++ b/src/ZF/UNITY/Constrains.thy	Sun Jul 29 14:30:07 2007 +0200
@@ -533,7 +533,7 @@
 val Always_Int_rule = foldr1 (fn (th1,th2) => [th1,th2] MRS Always_Int_I);
 
 (*To allow expansion of the program's definition when appropriate*)
-val program_defs_ref = ref ([]: thm list);
+structure ProgramDefs = NamedThmsFun(val name = "program" val description = "program definitions");
 
 (*proves "co" properties when the program is specified*)
 
@@ -549,7 +549,7 @@
               (* Three subgoals *)
               rewrite_goal_tac [st_set_def] 3,
               REPEAT (force_tac css 2),
-              full_simp_tac (ss addsimps !program_defs_ref) 1,
+              full_simp_tac (ss addsimps (ProgramDefs.get ctxt)) 1,
               ALLGOALS (clarify_tac cs),
               REPEAT (FIRSTGOAL (etac disjE)),
               ALLGOALS (clarify_tac cs),
@@ -564,6 +564,8 @@
     rtac AlwaysI i THEN force_tac (local_clasimpset_of ctxt) i THEN constrains_tac ctxt i;
 *}
 
+setup ProgramDefs.setup
+
 method_setup safety = {*
   Method.ctxt_args (fn ctxt =>
     Method.SIMPLE_METHOD' (constrains_tac ctxt)) *}
diff -r 248da5f0e735 -r 896fb015079c src/ZF/UNITY/Mutex.thy
--- a/src/ZF/UNITY/Mutex.thy	Sun Jul 29 14:30:06 2007 +0200
+++ b/src/ZF/UNITY/Mutex.thy	Sun Jul 29 14:30:07 2007 +0200
@@ -149,10 +149,7 @@
 
 
 declare Mutex_def [THEN def_prg_Init, simp]
-ML
-{*
-program_defs_ref := [thm"Mutex_def"]
-*}
+declare Mutex_def [program]
 
 declare  U0_def [THEN def_act_simp, simp]
 declare  U1_def [THEN def_act_simp, simp]
diff -r 248da5f0e735 -r 896fb015079c src/ZF/UNITY/SubstAx.thy
--- a/src/ZF/UNITY/SubstAx.thy	Sun Jul 29 14:30:06 2007 +0200
+++ b/src/ZF/UNITY/SubstAx.thy	Sun Jul 29 14:30:07 2007 +0200
@@ -412,7 +412,7 @@
                   REPEAT (ares_tac [LeadsTo_Basis, leadsTo_Basis,
                                     EnsuresI, ensuresI] 1),
               (*now there are two subgoals: co & transient*)
-              simp_tac (ss addsimps !program_defs_ref) 2,
+              simp_tac (ss addsimps (ProgramDefs.get ctxt)) 2,
               res_inst_tac [("act", sact)] transientI 2,
                  (*simplify the command's domain*)
               simp_tac (ss addsimps [domain_def]) 3,