src/HOL/NanoJava/Term.thy

   This_neq_Par [simp]: "This \<noteq> Par"
   Par_neq_Res  [simp]: "Par \<noteq> Res"
   Res_neq_This [simp]: "Res \<noteq> This"
 *)
 
-datatype stmt
+datatype_new stmt
   = Skip                   --{* empty statement *}
   | Comp       stmt stmt   ("_;; _"             [91,90   ] 90)
   | Cond expr  stmt stmt   ("If '(_') _ Else _" [ 3,91,91] 91)
   | Loop vname stmt        ("While '(_') _"     [ 3,91   ] 91)
   | LAss vname expr        ("_ :== _"           [99,   95] 94) --{* local assignment *}