1.1 --- a/src/HOL/MicroJava/J/JListExample.thy	Thu Dec 20 16:53:51 2001 +0100
     1.2 +++ b/src/HOL/MicroJava/J/JListExample.thy	Thu Dec 20 17:08:55 2001 +0100
     1.3 @@ -91,7 +91,7 @@
     1.4  *}
     1.5  
     1.6  generate_code
     1.7 -  test = "query (example_prg\<turnstile>Norm (Map.empty, Map.empty)
     1.8 +  test = "example_prg\<turnstile>Norm (Map.empty, Map.empty)
     1.9      -(Expr (l1_name::=NewC list_name);;
    1.10        Expr ({list_name}(LAcc l1_name)..val_name:=Lit (Intg 1));;
    1.11        Expr (l2_name::=NewC list_name);;
    1.12 @@ -105,7 +105,7 @@
    1.13        Expr ({list_name}(LAcc l1_name)..
    1.14          append_name({[RefT (ClassT list_name)]}[LAcc l3_name]));;
    1.15        Expr ({list_name}(LAcc l1_name)..
    1.16 -        append_name({[RefT (ClassT list_name)]}[LAcc l4_name])))-> s1)"
    1.17 +        append_name({[RefT (ClassT list_name)]}[LAcc l4_name])))-> _"
    1.18  
    1.19  subsection {* Big step execution *}
    1.20  

     2.1 --- a/src/HOL/Tools/inductive_codegen.ML	Thu Dec 20 16:53:51 2001 +0100
     2.2 +++ b/src/HOL/Tools/inductive_codegen.ML	Thu Dec 20 17:08:55 2001 +0100
     2.3 @@ -482,8 +482,8 @@
     2.4         None => None
     2.5       | Some (names, intrs) =>
     2.6           let
     2.7 -          fun mk_mode (((ts, mode), i), Var _) = ((ts, mode), i+1)
     2.8 -            | mk_mode (((ts, mode), i), Free _) = ((ts, mode), i+1)
     2.9 +          fun mk_mode (((ts, mode), i), Const ("dummy_pattern", _)) =
    2.10 +                ((ts, mode), i+1)
    2.11              | mk_mode (((ts, mode), i), t) = ((ts @ [t], mode @ [i]), i+1);
    2.12  
    2.13             val gr1 = mk_extra_defs thy
    2.14 @@ -508,12 +508,11 @@
    2.15    | _ => None);
    2.16  
    2.17  fun inductive_codegen thy gr dep brack (Const ("op :", _) $ t $ u) =
    2.18 -      (case mk_ind_call thy gr dep t u false of
    2.19 +      ((case mk_ind_call thy gr dep (Term.no_dummy_patterns t) u false of
    2.20           None => None
    2.21         | Some (gr', call_p) => Some (gr', (if brack then parens else I)
    2.22             (Pretty.block [Pretty.str "?! (", call_p, Pretty.str ")"])))
    2.23 -  | inductive_codegen thy gr dep brack (Free ("query", _) $ (Const ("op :", _) $ t $ u)) =
    2.24 -      mk_ind_call thy gr dep t u true
    2.25 +        handle TERM _ => mk_ind_call thy gr dep t u true)
    2.26    | inductive_codegen thy gr dep brack _ = None;
    2.27  
    2.28  val setup =