diff -r cab43c4a96d2 -r bc5bf9e9ada2 prio/PrioGDef.thy
--- a/prio/PrioGDef.thy	Sat Feb 11 09:14:14 2012 +0000
+++ b/prio/PrioGDef.thy	Sat Feb 11 09:34:46 2012 +0000
@@ -176,8 +176,8 @@
   threads:
   *}
 record schedule_state = 
-    waiting_queue :: "cs \<Rightarrow> thread list" -- {* The function assigning waiting queue. *}
-    cur_preced :: "thread \<Rightarrow> precedence" -- {* The function assigning precedence. *}
+    wq_fun :: "cs \<Rightarrow> thread list" -- {* The function assigning waiting queue. *}
+    cprec_fun :: "thread \<Rightarrow> precedence" -- {* The function assigning precedence. *}
 
 text {* \noindent 
   The following
@@ -220,7 +220,7 @@
   *}
 fun schs :: "state \<Rightarrow> schedule_state"
   where 
-  "schs [] = (| waiting_queue = \<lambda> cs. [],  cur_preced = (\<lambda>_. Prc 0 0) |)" |
+  "schs [] = (| wq_fun = \<lambda> cs. [],  cprec_fun = (\<lambda>_. Prc 0 0) |)" |
 
   -- {*
   \begin{minipage}{0.9\textwidth}
@@ -248,22 +248,22 @@
   \end{minipage}
      *}
    "schs (Create th prio # s) = 
-       (let wq = waiting_queue (schs s) in
-          (|waiting_queue = wq, cur_preced = cpreced wq (Create th prio # s)|))"
+       (let wq = wq_fun (schs s) in
+          (|wq_fun = wq, cprec_fun = cpreced wq (Create th prio # s)|))"
 |  "schs (Exit th # s) = 
-       (let wq = waiting_queue (schs s) in
-          (|waiting_queue = wq, cur_preced = cpreced wq (Exit th # s)|))"
+       (let wq = wq_fun (schs s) in
+          (|wq_fun = wq, cprec_fun = cpreced wq (Exit th # s)|))"
 |  "schs (Set th prio # s) = 
-       (let wq = waiting_queue (schs s) in
-          (|waiting_queue = wq, cur_preced = cpreced wq (Set th prio # s)|))"
+       (let wq = wq_fun (schs s) in
+          (|wq_fun = wq, cprec_fun = cpreced wq (Set th prio # s)|))"
 |  "schs (P th cs # s) = 
-       (let wq = waiting_queue (schs s) in
+       (let wq = wq_fun (schs s) in
         let new_wq = wq(cs := (wq cs @ [th])) in
-          (|waiting_queue = new_wq, cur_preced = cpreced new_wq (P th cs # s)|))"
+          (|wq_fun = new_wq, cprec_fun = cpreced new_wq (P th cs # s)|))"
 |  "schs (V th cs # s) = 
-       (let wq = waiting_queue (schs s) in
+       (let wq = wq_fun (schs s) in
         let new_wq = wq(cs := release (wq cs)) in
-          (|waiting_queue = new_wq, cur_preced = cpreced new_wq (V th cs # s)|))"
+          (|wq_fun = new_wq, cprec_fun = cpreced new_wq (V th cs # s)|))"
 
 lemma cpreced_initial: 
   "cpreced (\<lambda> cs. []) [] = (\<lambda>_. (Prc 0 0))"
@@ -274,7 +274,7 @@
 
 lemma sch_old_def:
   "schs (e#s) = (let ps = schs s in 
-                  let pwq = waiting_queue ps in 
+                  let pwq = wq_fun ps in 
                   let nwq = case e of
                              P th cs \<Rightarrow>  pwq(cs:=(pwq cs @ [th])) |
                              V th cs \<Rightarrow> let nq = case (pwq cs) of
@@ -283,7 +283,7 @@
                                             in pwq(cs:=nq)                 |
                               _ \<Rightarrow> pwq
                   in let ncp = cpreced nwq (e#s) in 
-                     \<lparr>waiting_queue = nwq, cur_preced = ncp\<rparr>
+                     \<lparr>wq_fun = nwq, cprec_fun = ncp\<rparr>
                  )"
 apply(cases e)
 apply(simp_all)
@@ -292,16 +292,16 @@
 
 text {* 
   \noindent
-  The following @{text "wq"} is a shorthand for @{text "waiting_queue"}. 
+  The following @{text "wq"} is a shorthand for @{text "wq_fun"}. 
   *}
 definition wq :: "state \<Rightarrow> cs \<Rightarrow> thread list" 
-  where "wq s = waiting_queue (schs s)"
+  where "wq s = wq_fun (schs s)"
 
 text {* \noindent 
-  The following @{text "cp"} is a shorthand for @{text "cur_preced"}. 
+  The following @{text "cp"} is a shorthand for @{text "cprec_fun"}. 
   *}
 definition cp :: "state \<Rightarrow> thread \<Rightarrow> precedence"
-  where "cp s = cur_preced (schs s)"
+  where "cp s = cprec_fun (schs s)"
 
 text {* \noindent
   Functions @{text "holding"}, @{text "waiting"}, @{text "depend"} and