modernized primrecs

--- a/src/HOL/MicroJava/BV/Typing_Framework_JVM.thy	Tue Sep 28 12:47:55 2010 +0200
+++ b/src/HOL/MicroJava/BV/Typing_Framework_JVM.thy	Tue Sep 28 12:47:55 2010 +0200
@@ -18,11 +18,11 @@
 
 
 section {*  Executability of @{term check_bounded} *}
-consts
-  list_all'_rec :: "('a \<Rightarrow> nat \<Rightarrow> bool) \<Rightarrow> nat \<Rightarrow> 'a list \<Rightarrow> bool"
-primrec
+
+primrec list_all'_rec :: "('a \<Rightarrow> nat \<Rightarrow> bool) \<Rightarrow> nat \<Rightarrow> 'a list \<Rightarrow> bool"
+where
   "list_all'_rec P n []     = True"
-  "list_all'_rec P n (x#xs) = (P x n \<and> list_all'_rec P (Suc n) xs)"
+| "list_all'_rec P n (x#xs) = (P x n \<and> list_all'_rec P (Suc n) xs)"
 
 definition list_all' :: "('a \<Rightarrow> nat \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> bool" where
   "list_all' P xs \<equiv> list_all'_rec P 0 xs"

--- a/src/HOL/MicroJava/Comp/TranslComp.thy	Tue Sep 28 12:47:55 2010 +0200
+++ b/src/HOL/MicroJava/Comp/TranslComp.thy	Tue Sep 28 12:47:55 2010 +0200
@@ -8,71 +8,69 @@
 
 
 (* parameter java_mb only serves to define function index later *)
-consts
- compExpr  :: "java_mb => expr      => instr list"
- compExprs :: "java_mb => expr list => instr list"
- compStmt  :: "java_mb => stmt      => instr list"
-
 
 
 (**********************************************************************)
 (** code generation for expressions **)
 
-primrec
+primrec compExpr :: "java_mb => expr => instr list"
+  and compExprs :: "java_mb => expr list => instr list"
+where
+
 (*class instance creation*)
-"compExpr jmb (NewC c) = [New c]"
+"compExpr jmb (NewC c) = [New c]" |
 
 (*type cast*)
-"compExpr jmb (Cast c e) = compExpr jmb e @ [Checkcast c]" 
+"compExpr jmb (Cast c e) = compExpr jmb e @ [Checkcast c]" |
 
 
 (*literals*)
-"compExpr jmb (Lit val) = [LitPush val]" 
+"compExpr jmb (Lit val) = [LitPush val]" |
 
       
 (* binary operation *)                         
 "compExpr jmb (BinOp bo e1 e2) = compExpr jmb e1 @ compExpr jmb e2 @ 
   (case bo of Eq => [Ifcmpeq 3,LitPush(Bool False),Goto 2,LitPush(Bool True)]
-            | Add => [IAdd])" 
+            | Add => [IAdd])" |
 
 (*local variable*)
-"compExpr jmb (LAcc vn) = [Load (index jmb vn)]" 
+"compExpr jmb (LAcc vn) = [Load (index jmb vn)]" |
 
 
 (*assignement*)
-"compExpr jmb (vn::=e) = compExpr jmb e @ [Dup , Store (index jmb vn)]" 
+"compExpr jmb (vn::=e) = compExpr jmb e @ [Dup , Store (index jmb vn)]" |
 
 
 (*field access*)
-"compExpr jmb ( {cn}e..fn ) = compExpr jmb e @ [Getfield fn cn]"
+"compExpr jmb ( {cn}e..fn ) = compExpr jmb e @ [Getfield fn cn]" |
 
 
 (*field assignement - expected syntax:  {_}_.._:=_ *)
 "compExpr jmb (FAss cn e1 fn e2 ) = 
-       compExpr jmb e1 @ compExpr jmb e2 @ [Dup_x1 , Putfield fn cn]"
+       compExpr jmb e1 @ compExpr jmb e2 @ [Dup_x1 , Putfield fn cn]" |
 
 
 (*method call*)
 "compExpr jmb (Call cn e1 mn X ps) = 
-        compExpr jmb e1 @ compExprs jmb ps @ [Invoke cn mn X]"
+        compExpr jmb e1 @ compExprs jmb ps @ [Invoke cn mn X]" |
 
 
 (** code generation expression lists **)
 
-"compExprs jmb []     = []"
+"compExprs jmb []     = []" |
 
 "compExprs jmb (e#es) = compExpr jmb e @ compExprs jmb es"
 
-  
 
-primrec
+primrec compStmt :: "java_mb => stmt => instr list" where
+
 (** code generation for statements **)
 
-"compStmt jmb Skip = []"                        
+"compStmt jmb Skip = []" |
 
-"compStmt jmb (Expr e) = ((compExpr jmb e) @ [Pop])"
+"compStmt jmb (Expr e) = ((compExpr jmb e) @ [Pop])" |
 
-"compStmt jmb (c1;; c2) = ((compStmt jmb c1) @ (compStmt jmb c2))"
+"compStmt jmb (c1;; c2) = ((compStmt jmb c1) @ (compStmt jmb c2))" |
 
 "compStmt jmb (If(e) c1 Else c2) =
         (let cnstf = LitPush (Bool False);
@@ -82,7 +80,7 @@
              test  = Ifcmpeq (int(length thn +2)); 
              thnex = Goto (int(length els +1))
          in
-         [cnstf] @ cnd @ [test] @ thn @ [thnex] @ els)"
+         [cnstf] @ cnd @ [test] @ thn @ [thnex] @ els)" |
 
 "compStmt jmb (While(e) c) =
         (let cnstf = LitPush (Bool False);

--- a/src/HOL/MicroJava/Comp/TranslCompTp.thy	Tue Sep 28 12:47:55 2010 +0200
+++ b/src/HOL/MicroJava/Comp/TranslCompTp.thy	Tue Sep 28 12:47:55 2010 +0200
@@ -45,16 +45,6 @@
   sttp_of :: "method_type \<times> state_type \<Rightarrow> state_type"
   where "sttp_of == snd"
 
-consts
-  compTpExpr  :: "java_mb \<Rightarrow> java_mb prog \<Rightarrow> expr
-                   \<Rightarrow> state_type \<Rightarrow> method_type \<times> state_type"
-
-  compTpExprs :: "java_mb \<Rightarrow> java_mb prog \<Rightarrow> expr list
-                   \<Rightarrow> state_type \<Rightarrow> method_type \<times> state_type"
-
-  compTpStmt  :: "java_mb \<Rightarrow> java_mb prog \<Rightarrow> stmt
-                   \<Rightarrow> state_type \<Rightarrow> method_type \<times> state_type"
-
 definition nochangeST :: "state_type \<Rightarrow> method_type \<times> state_type" where
   "nochangeST sttp == ([Some sttp], sttp)"
 
@@ -80,60 +70,45 @@
 
 (* Expressions *)
 
-primrec
-
+primrec compTpExpr :: "java_mb \<Rightarrow> java_mb prog \<Rightarrow> expr \<Rightarrow>
+    state_type \<Rightarrow> method_type \<times> state_type"
+  and compTpExprs :: "java_mb \<Rightarrow> java_mb prog \<Rightarrow> expr list \<Rightarrow>
+    state_type \<Rightarrow> method_type \<times> state_type"
+where
   "compTpExpr jmb G (NewC c) = pushST [Class c]"
-
-  "compTpExpr jmb G (Cast c e) = 
-  (compTpExpr jmb G e) \<box> (replST 1 (Class c))"
-
-  "compTpExpr jmb G (Lit val) = pushST [the (typeof (\<lambda>v. None) val)]"
-
-  "compTpExpr jmb G (BinOp bo e1 e2) = 
+| "compTpExpr jmb G (Cast c e) = (compTpExpr jmb G e) \<box> (replST 1 (Class c))"
+| "compTpExpr jmb G (Lit val) = pushST [the (typeof (\<lambda>v. None) val)]"
+| "compTpExpr jmb G (BinOp bo e1 e2) =
      (compTpExpr jmb G e1) \<box> (compTpExpr jmb G e2) \<box> 
      (case bo of 
        Eq => popST 2 \<box> pushST [PrimT Boolean] \<box> popST 1 \<box> pushST [PrimT Boolean]
      | Add => replST 2 (PrimT Integer))"
-
-  "compTpExpr jmb G (LAcc vn) = (\<lambda> (ST, LT). 
+| "compTpExpr jmb G (LAcc vn) = (\<lambda> (ST, LT). 
       pushST [ok_val (LT ! (index jmb vn))] (ST, LT))"
-
-  "compTpExpr jmb G (vn::=e) = 
+| "compTpExpr jmb G (vn::=e) = 
       (compTpExpr jmb G e) \<box> dupST \<box> (popST 1)"
-
-
-  "compTpExpr jmb G ( {cn}e..fn ) = 
+| "compTpExpr jmb G ( {cn}e..fn ) = 
       (compTpExpr jmb G e) \<box> replST 1 (snd (the (field (G,cn) fn)))"
-
-  "compTpExpr jmb G (FAss cn e1 fn e2 ) = 
+| "compTpExpr jmb G (FAss cn e1 fn e2 ) = 
       (compTpExpr jmb G e1) \<box> (compTpExpr jmb G e2) \<box> dup_x1ST \<box> (popST 2)"
-
-
-  "compTpExpr jmb G ({C}a..mn({fpTs}ps)) =
+| "compTpExpr jmb G ({C}a..mn({fpTs}ps)) =
        (compTpExpr jmb G a) \<box> (compTpExprs jmb G ps) \<box> 
        (replST ((length ps) + 1) (method_rT (the (method (G,C) (mn,fpTs)))))"
-
-
-(* Expression lists *)
-
-  "compTpExprs jmb G [] = comb_nil"
-
-  "compTpExprs jmb G (e#es) = (compTpExpr jmb G e) \<box> (compTpExprs jmb G es)"
+| "compTpExprs jmb G [] = comb_nil"
+| "compTpExprs jmb G (e#es) = (compTpExpr jmb G e) \<box> (compTpExprs jmb G es)"
 
 
 (* Statements *)
-primrec
-   "compTpStmt jmb G Skip = comb_nil"
-
-   "compTpStmt jmb G (Expr e) =  (compTpExpr jmb G e) \<box> popST 1"
-
-   "compTpStmt jmb G (c1;; c2) = (compTpStmt jmb G c1) \<box> (compTpStmt jmb G c2)"
-
-   "compTpStmt jmb G (If(e) c1 Else c2) = 
+primrec compTpStmt :: "java_mb \<Rightarrow> java_mb prog \<Rightarrow> stmt \<Rightarrow> 
+    state_type \<Rightarrow> method_type \<times> state_type"
+where
+  "compTpStmt jmb G Skip = comb_nil"
+| "compTpStmt jmb G (Expr e) =  (compTpExpr jmb G e) \<box> popST 1"
+| "compTpStmt jmb G (c1;; c2) = (compTpStmt jmb G c1) \<box> (compTpStmt jmb G c2)"
+| "compTpStmt jmb G (If(e) c1 Else c2) = 
       (pushST [PrimT Boolean]) \<box> (compTpExpr jmb G e) \<box> popST 2 \<box>
       (compTpStmt jmb G c1) \<box> nochangeST \<box> (compTpStmt jmb G c2)"
-
-   "compTpStmt jmb G (While(e) c) = 
+| "compTpStmt jmb G (While(e) c) = 
       (pushST [PrimT Boolean]) \<box> (compTpExpr jmb G e) \<box> popST 2 \<box>
       (compTpStmt jmb G c) \<box> nochangeST"
 
@@ -141,13 +116,11 @@
                    \<Rightarrow> state_type \<Rightarrow> method_type \<times> state_type" where
   "compTpInit jmb == (\<lambda> (vn,ty). (pushST [ty]) \<box>  (storeST (index jmb vn) ty))"
 
-consts
-  compTpInitLvars :: "[java_mb, (vname \<times> ty) list] 
-                   \<Rightarrow> state_type \<Rightarrow> method_type \<times> state_type"
-
-primrec 
+primrec compTpInitLvars :: "[java_mb, (vname \<times> ty) list] \<Rightarrow>
+    state_type \<Rightarrow> method_type \<times> state_type"
+where
   "compTpInitLvars jmb [] = comb_nil"
-  "compTpInitLvars jmb (lv#lvars) = (compTpInit jmb lv) \<box> (compTpInitLvars jmb lvars)"
+| "compTpInitLvars jmb (lv#lvars) = (compTpInit jmb lv) \<box> (compTpInitLvars jmb lvars)"
 
 definition start_ST :: "opstack_type" where
   "start_ST == []"

--- a/src/HOL/MicroJava/DFA/Err.thy	Tue Sep 28 12:47:55 2010 +0200
+++ b/src/HOL/MicroJava/DFA/Err.thy	Tue Sep 28 12:47:55 2010 +0200
@@ -47,11 +47,9 @@
   where "err_semilat L == semilat(Err.sl L)"
 
 
-consts
-  strict  :: "('a \<Rightarrow> 'b err) \<Rightarrow> ('a err \<Rightarrow> 'b err)"
-primrec
+primrec strict :: "('a \<Rightarrow> 'b err) \<Rightarrow> ('a err \<Rightarrow> 'b err)" where
   "strict f Err    = Err"
-  "strict f (OK x) = f x"
+| "strict f (OK x) = f x"
 
 lemma strict_Some [simp]: 
   "(strict f x = OK y) = (\<exists> z. x = OK z \<and> f z = OK y)"

--- a/src/HOL/MicroJava/J/Value.thy	Tue Sep 28 12:47:55 2010 +0200
+++ b/src/HOL/MicroJava/J/Value.thy	Tue Sep 28 12:47:55 2010 +0200
@@ -22,31 +22,22 @@
                    of clash with HOL/Set.thy" 
   | Addr loc    -- "addresses, i.e. locations of objects "
 
-consts
-  the_Bool :: "val => bool"
-  the_Intg :: "val => int"
-  the_Addr :: "val => loc"
-
-primrec
+primrec the_Bool :: "val => bool" where
   "the_Bool (Bool b) = b"
 
-primrec
+primrec the_Intg :: "val => int" where
   "the_Intg (Intg i) = i"
 
-primrec
+primrec the_Addr :: "val => loc" where
   "the_Addr (Addr a) = a"
 
-consts
-  defpval :: "prim_ty => val"  -- "default value for primitive types"
-  default_val :: "ty => val"   -- "default value for all types"
-
-primrec
+primrec defpval :: "prim_ty => val"  -- "default value for primitive types" where
   "defpval Void    = Unit"
-  "defpval Boolean = Bool False"
-  "defpval Integer = Intg 0"
+| "defpval Boolean = Bool False"
+| "defpval Integer = Intg 0"
 
-primrec
+primrec default_val :: "ty => val"   -- "default value for all types" where
   "default_val (PrimT pt) = defpval pt"
-  "default_val (RefT  r ) = Null"
+| "default_val (RefT  r ) = Null"
 
 end

--- a/src/HOL/MicroJava/J/WellType.thy	Tue Sep 28 12:47:55 2010 +0200
+++ b/src/HOL/MicroJava/J/WellType.thy	Tue Sep 28 12:47:55 2010 +0200
@@ -73,15 +73,13 @@
                          THEN max_spec2appl_meths, THEN appl_methsD]
 
 
-consts
-  typeof :: "(loc => ty option) => val => ty option"
-
-primrec
+primrec typeof :: "(loc => ty option) => val => ty option"
+where
   "typeof dt  Unit    = Some (PrimT Void)"
-  "typeof dt  Null    = Some NT"
-  "typeof dt (Bool b) = Some (PrimT Boolean)"
-  "typeof dt (Intg i) = Some (PrimT Integer)"
-  "typeof dt (Addr a) = dt a"
+| "typeof dt  Null    = Some NT"
+| "typeof dt (Bool b) = Some (PrimT Boolean)"
+| "typeof dt (Intg i) = Some (PrimT Integer)"
+| "typeof dt (Addr a) = dt a"
 
 lemma is_type_typeof [rule_format (no_asm), simp]: 
   "(\<forall>a. v \<noteq> Addr a) --> (\<exists>T. typeof t v = Some T \<and> is_type G T)"

--- a/src/HOL/MicroJava/JVM/JVMExceptions.thy	Tue Sep 28 12:47:55 2010 +0200
+++ b/src/HOL/MicroJava/JVM/JVMExceptions.thy	Tue Sep 28 12:47:55 2010 +0200
@@ -13,12 +13,11 @@
                  start_pc <= pc \<and> pc < end_pc \<and> G\<turnstile> cn \<preceq>C catch_type"
 
 
-consts
-  match_exception_table :: "jvm_prog \<Rightarrow> cname \<Rightarrow> p_count \<Rightarrow> exception_table
-                          \<Rightarrow> p_count option"
-primrec
+primrec match_exception_table :: "jvm_prog \<Rightarrow> cname \<Rightarrow> p_count \<Rightarrow> exception_table
+    \<Rightarrow> p_count option"
+where
   "match_exception_table G cn pc []     = None"
-  "match_exception_table G cn pc (e#es) = (if match_exception_entry G cn pc e
+| "match_exception_table G cn pc (e#es) = (if match_exception_entry G cn pc e
                                            then Some (fst (snd (snd e))) 
                                            else match_exception_table G cn pc es)"
 
@@ -27,11 +26,11 @@
   where "ex_table_of m == snd (snd (snd m))"
 
 
-consts
-  find_handler :: "jvm_prog \<Rightarrow> val option \<Rightarrow> aheap \<Rightarrow> frame list \<Rightarrow> jvm_state"
-primrec
+primrec find_handler :: "jvm_prog \<Rightarrow> val option \<Rightarrow> aheap \<Rightarrow> frame list
+    \<Rightarrow> jvm_state"
+where
   "find_handler G xcpt hp [] = (xcpt, hp, [])"
-  "find_handler G xcpt hp (fr#frs) = 
+| "find_handler G xcpt hp (fr#frs) = 
       (case xcpt of
          None \<Rightarrow> (None, hp, fr#frs)
        | Some xc \<Rightarrow> 

--- a/src/HOL/MicroJava/JVM/JVMExecInstr.thy	Tue Sep 28 12:47:55 2010 +0200
+++ b/src/HOL/MicroJava/JVM/JVMExecInstr.thy	Tue Sep 28 12:47:55 2010 +0200
@@ -1,5 +1,4 @@
 (*  Title:      HOL/MicroJava/JVM/JVMExecInstr.thy
-    ID:         $Id$
     Author:     Cornelia Pusch, Gerwin Klein
     Copyright   1999 Technische Universitaet Muenchen
 *)
@@ -11,18 +10,16 @@
 theory JVMExecInstr imports JVMInstructions JVMState begin
 
 
-consts
-  exec_instr :: "[instr, jvm_prog, aheap, opstack, locvars, 
-                  cname, sig, p_count, frame list] => jvm_state"
-primrec
+primrec exec_instr :: "[instr, jvm_prog, aheap, opstack, locvars, cname, sig, p_count, frame list] => jvm_state"
+where
  "exec_instr (Load idx) G hp stk vars Cl sig pc frs = 
-      (None, hp, ((vars ! idx) # stk, vars, Cl, sig, pc+1)#frs)"
+      (None, hp, ((vars ! idx) # stk, vars, Cl, sig, pc+1)#frs)" |
 
  "exec_instr (Store idx) G hp stk vars Cl sig pc frs = 
-      (None, hp, (tl stk, vars[idx:=hd stk], Cl, sig, pc+1)#frs)"
+      (None, hp, (tl stk, vars[idx:=hd stk], Cl, sig, pc+1)#frs)" |
 
  "exec_instr (LitPush v) G hp stk vars Cl sig pc frs = 
-      (None, hp, (v # stk, vars, Cl, sig, pc+1)#frs)"
+      (None, hp, (v # stk, vars, Cl, sig, pc+1)#frs)" |
 
  "exec_instr (New C) G hp stk vars Cl sig pc frs = 
   (let (oref,xp') = new_Addr hp;
@@ -30,7 +27,7 @@
        hp'  = if xp'=None then hp(oref \<mapsto> (C,fs)) else hp;
        pc'  = if xp'=None then pc+1 else pc
    in 
-      (xp', hp', (Addr oref#stk, vars, Cl, sig, pc')#frs))"
+      (xp', hp', (Addr oref#stk, vars, Cl, sig, pc')#frs))" |
 
  "exec_instr (Getfield F C) G hp stk vars Cl sig pc frs = 
   (let oref = hd stk;
@@ -38,7 +35,7 @@
        (oc,fs)  = the(hp(the_Addr oref));
        pc'  = if xp'=None then pc+1 else pc
    in
-      (xp', hp, (the(fs(F,C))#(tl stk), vars, Cl, sig, pc')#frs))"
+      (xp', hp, (the(fs(F,C))#(tl stk), vars, Cl, sig, pc')#frs))" |
 
  "exec_instr (Putfield F C) G hp stk vars Cl sig pc frs = 
   (let (fval,oref)= (hd stk, hd(tl stk));
@@ -48,7 +45,7 @@
        hp'  = if xp'=None then hp(a \<mapsto> (oc, fs((F,C) \<mapsto> fval))) else hp;
        pc'  = if xp'=None then pc+1 else pc
    in
-      (xp', hp', (tl (tl stk), vars, Cl, sig, pc')#frs))"
+      (xp', hp', (tl (tl stk), vars, Cl, sig, pc')#frs))" |
 
  "exec_instr (Checkcast C) G hp stk vars Cl sig pc frs =
   (let oref = hd stk;
@@ -56,7 +53,7 @@
        stk' = if xp'=None then stk else tl stk;
        pc'  = if xp'=None then pc+1 else pc
    in
-      (xp', hp, (stk', vars, Cl, sig, pc')#frs))"
+      (xp', hp, (stk', vars, Cl, sig, pc')#frs))" |
 
  "exec_instr (Invoke C mn ps) G hp stk vars Cl sig pc frs =
   (let n    = length ps;
@@ -69,7 +66,7 @@
                 [([],rev argsoref@replicate mxl undefined,dc,(mn,ps),0)]
               else []
    in 
-      (xp', hp, frs'@(stk, vars, Cl, sig, pc)#frs))" 
+      (xp', hp, frs'@(stk, vars, Cl, sig, pc)#frs))" |
   -- "Because exception handling needs the pc of the Invoke instruction,"
   -- "Invoke doesn't change stk and pc yet (@{text Return} does that)."
 
@@ -82,42 +79,42 @@
    in 
       (None, hp, (val#(drop (n+1) stk),loc,C,sig,pc+1)#tl frs))"
   -- "Return drops arguments from the caller's stack and increases"
-  -- "the program counter in the caller"
+  -- "the program counter in the caller" |
 
  "exec_instr Pop G hp stk vars Cl sig pc frs = 
-      (None, hp, (tl stk, vars, Cl, sig, pc+1)#frs)"
+      (None, hp, (tl stk, vars, Cl, sig, pc+1)#frs)" |
 
  "exec_instr Dup G hp stk vars Cl sig pc frs = 
-      (None, hp, (hd stk # stk, vars, Cl, sig, pc+1)#frs)"
+      (None, hp, (hd stk # stk, vars, Cl, sig, pc+1)#frs)" |
 
  "exec_instr Dup_x1 G hp stk vars Cl sig pc frs = 
       (None, hp, (hd stk # hd (tl stk) # hd stk # (tl (tl stk)), 
-                  vars, Cl, sig, pc+1)#frs)"
+                  vars, Cl, sig, pc+1)#frs)" |
 
  "exec_instr Dup_x2 G hp stk vars Cl sig pc frs = 
       (None, hp, 
        (hd stk # hd (tl stk) # (hd (tl (tl stk))) # hd stk # (tl (tl (tl stk))),
-       vars, Cl, sig, pc+1)#frs)"
+       vars, Cl, sig, pc+1)#frs)" |
 
  "exec_instr Swap G hp stk vars Cl sig pc frs =
   (let (val1,val2) = (hd stk,hd (tl stk))
    in
-      (None, hp, (val2#val1#(tl (tl stk)), vars, Cl, sig, pc+1)#frs))"
+      (None, hp, (val2#val1#(tl (tl stk)), vars, Cl, sig, pc+1)#frs))" |
 
  "exec_instr IAdd G hp stk vars Cl sig pc frs =
   (let (val1,val2) = (hd stk,hd (tl stk))
    in
       (None, hp, (Intg ((the_Intg val1)+(the_Intg val2))#(tl (tl stk)), 
-       vars, Cl, sig, pc+1)#frs))"
+       vars, Cl, sig, pc+1)#frs))" |
 
  "exec_instr (Ifcmpeq i) G hp stk vars Cl sig pc frs =
   (let (val1,val2) = (hd stk, hd (tl stk));
      pc' = if val1 = val2 then nat(int pc+i) else pc+1
    in
-      (None, hp, (tl (tl stk), vars, Cl, sig, pc')#frs))"
+      (None, hp, (tl (tl stk), vars, Cl, sig, pc')#frs))" |
 
  "exec_instr (Goto i) G hp stk vars Cl sig pc frs =
-      (None, hp, (stk, vars, Cl, sig, nat(int pc+i))#frs)"
+      (None, hp, (stk, vars, Cl, sig, nat(int pc+i))#frs)" |
 
  "exec_instr Throw G hp stk vars Cl sig pc frs =
   (let xcpt  = raise_system_xcpt (hd stk = Null) NullPointer;

--- a/src/HOL/NanoJava/Example.thy	Tue Sep 28 12:47:55 2010 +0200
+++ b/src/HOL/NanoJava/Example.thy	Tue Sep 28 12:47:55 2010 +0200
@@ -5,7 +5,9 @@
 
 header "Example"
 
-theory Example imports Equivalence begin
+theory Example
+imports Equivalence
+begin
 
 text {*
 
@@ -89,9 +91,9 @@
 
 subsection "``atleast'' relation for interpretation of Nat ``values''"
 
-consts Nat_atleast :: "state \<Rightarrow> val \<Rightarrow> nat \<Rightarrow> bool" ("_:_ \<ge> _" [51, 51, 51] 50)
-primrec "s:x\<ge>0     = (x\<noteq>Null)"
-        "s:x\<ge>Suc n = (\<exists>a. x=Addr a \<and> heap s a \<noteq> None \<and> s:get_field s a pred\<ge>n)"
+primrec Nat_atleast :: "state \<Rightarrow> val \<Rightarrow> nat \<Rightarrow> bool" ("_:_ \<ge> _" [51, 51, 51] 50) where
+  "s:x\<ge>0     = (x\<noteq>Null)"
+| "s:x\<ge>Suc n = (\<exists>a. x=Addr a \<and> heap s a \<noteq> None \<and> s:get_field s a pred\<ge>n)"
 
 lemma Nat_atleast_lupd [rule_format, simp]: 
  "\<forall>s v::val. lupd(x\<mapsto>y) s:v \<ge> n = (s:v \<ge> n)"

--- a/src/HOL/SET_Protocol/Cardholder_Registration.thy	Tue Sep 28 12:47:55 2010 +0200
+++ b/src/HOL/SET_Protocol/Cardholder_Registration.thy	Tue Sep 28 12:47:55 2010 +0200
@@ -21,44 +21,36 @@
 
 subsection{*Predicate Formalizing the Encryption Association between Keys *}
 
-consts
-  KeyCryptKey :: "[key, key, event list] => bool"
-
-primrec
-
-KeyCryptKey_Nil:
-  "KeyCryptKey DK K [] = False"
-
-KeyCryptKey_Cons:
+primrec KeyCryptKey :: "[key, key, event list] => bool"
+where
+  KeyCryptKey_Nil:
+    "KeyCryptKey DK K [] = False"
+| KeyCryptKey_Cons:
       --{*Says is the only important case.
         1st case: CR5, where KC3 encrypts KC2.
         2nd case: any use of priEK C.
         Revision 1.12 has a more complicated version with separate treatment of
           the dependency of KC1, KC2 and KC3 on priEK (CA i.)  Not needed since
           priEK C is never sent (and so can't be lost except at the start). *}
-  "KeyCryptKey DK K (ev # evs) =
-   (KeyCryptKey DK K evs |
-    (case ev of
-      Says A B Z =>
-       ((\<exists>N X Y. A \<noteq> Spy &
+    "KeyCryptKey DK K (ev # evs) =
+     (KeyCryptKey DK K evs |
+      (case ev of
+        Says A B Z =>
+         ((\<exists>N X Y. A \<noteq> Spy &
                  DK \<in> symKeys &
                  Z = {|Crypt DK {|Agent A, Nonce N, Key K, X|}, Y|}) |
-        (\<exists>C. DK = priEK C))
-    | Gets A' X => False
-    | Notes A' X => False))"
+          (\<exists>C. DK = priEK C))
+      | Gets A' X => False
+      | Notes A' X => False))"
 
 
 subsection{*Predicate formalizing the association between keys and nonces *}
 
-consts
-  KeyCryptNonce :: "[key, key, event list] => bool"
-
-primrec
-
-KeyCryptNonce_Nil:
-  "KeyCryptNonce EK K [] = False"
-
-KeyCryptNonce_Cons:
+primrec KeyCryptNonce :: "[key, key, event list] => bool"
+where
+  KeyCryptNonce_Nil:
+    "KeyCryptNonce EK K [] = False"
+| KeyCryptNonce_Cons:
   --{*Says is the only important case.
     1st case: CR3, where KC1 encrypts NC2 (distinct from CR5 due to EXH);
     2nd case: CR5, where KC3 encrypts NC3;

--- a/src/HOL/SET_Protocol/Event_SET.thy	Tue Sep 28 12:47:55 2010 +0200
+++ b/src/HOL/SET_Protocol/Event_SET.thy	Tue Sep 28 12:47:55 2010 +0200
@@ -35,15 +35,14 @@
 
 consts  (*Initial states of agents -- parameter of the construction*)
   initState :: "agent => msg set"
-  knows  :: "[agent, event list] => msg set"
 
 (* Message reception does not extend spy's knowledge because of
    reception invariant enforced by Reception rule in protocol definition*)
-primrec
-
-knows_Nil:
-  "knows A []       = initState A"
-knows_Cons:
+primrec knows :: "[agent, event list] => msg set"
+where
+  knows_Nil:
+    "knows A [] = initState A"
+| knows_Cons:
     "knows A (ev # evs) =
        (if A = Spy then
         (case ev of
@@ -63,15 +62,13 @@
 
 subsection{*Used Messages*}
 
-consts
+primrec used :: "event list => msg set"
+where
   (*Set of items that might be visible to somebody:
-    complement of the set of fresh items*)
-  used :: "event list => msg set"
-
-(* As above, message reception does extend used items *)
-primrec
+    complement of the set of fresh items.
+    As above, message reception does extend used items *)
   used_Nil:  "used []         = (UN B. parts (initState B))"
-  used_Cons: "used (ev # evs) =
+| used_Cons: "used (ev # evs) =
                  (case ev of
                     Says A B X => parts {X} Un (used evs)
                   | Gets A X   => used evs

--- a/src/HOL/SET_Protocol/Public_SET.thy	Tue Sep 28 12:47:55 2010 +0200
+++ b/src/HOL/SET_Protocol/Public_SET.thy	Tue Sep 28 12:47:55 2010 +0200
@@ -64,7 +64,11 @@
    RCA and CAs know their own respective keys;
    RCA (has already certified and therefore) knows all CAs public keys; 
    Spy knows all keys of all bad agents.*}
-primrec    
+
+overloading initState \<equiv> "initState"
+begin
+
+primrec initState where
 (*<*)
   initState_CA:
     "initState (CA i)  =
@@ -74,29 +78,31 @@
               Key (pubEK (CA i)), Key (pubSK (CA i)),
               Key (pubEK RCA), Key (pubSK RCA)})"
 
-  initState_Cardholder:
+| initState_Cardholder:
     "initState (Cardholder i)  =    
        {Key (priEK (Cardholder i)), Key (priSK (Cardholder i)),
         Key (pubEK (Cardholder i)), Key (pubSK (Cardholder i)),
         Key (pubEK RCA), Key (pubSK RCA)}"
 
-  initState_Merchant:
+| initState_Merchant:
     "initState (Merchant i)  =    
        {Key (priEK (Merchant i)), Key (priSK (Merchant i)),
         Key (pubEK (Merchant i)), Key (pubSK (Merchant i)),
         Key (pubEK RCA), Key (pubSK RCA)}"
 
-  initState_PG:
+| initState_PG:
     "initState (PG i)  = 
        {Key (priEK (PG i)), Key (priSK (PG i)),
         Key (pubEK (PG i)), Key (pubSK (PG i)),
         Key (pubEK RCA), Key (pubSK RCA)}"
 (*>*)
-  initState_Spy:
+| initState_Spy:
     "initState Spy = Key ` (invKey ` pubEK ` bad Un
                             invKey ` pubSK ` bad Un
                             range pubEK Un range pubSK)"
 
+end
+
 
 text{*Injective mapping from agents to PANs: an agent can have only one card*}