src/HOL/MicroJava/J/JListExample.thy

   let fun nr i = if p (hp (loc i)) then (loc i, none) else nr (i+1);
   in nr 0 end;
 *}
 
 generate_code
-  test = "example_prg\<turnstile>Norm (Map.empty, Map.empty)
+  test = "example_prg\<turnstile>Norm (empty, empty)
     -(Expr (l1_name::=NewC list_name);;
       Expr ({list_name}(LAcc l1_name)..val_name:=Lit (Intg 1));;
       Expr (l2_name::=NewC list_name);;
       Expr ({list_name}(LAcc l2_name)..val_name:=Lit (Intg 2));;
       Expr (l3_name::=NewC list_name);;