# HG changeset patch
# User berghofe
# Date 1008864535 -3600
# Node ID 9df4b3934487452b6f3d4ef25e169d543cfca1bf
# Parent  226873bffa3a17f2ad0c62ad8923af5cb825a464
Eliminated "query" syntax.

diff -r 226873bffa3a -r 9df4b3934487 src/HOL/MicroJava/J/JListExample.thy
--- a/src/HOL/MicroJava/J/JListExample.thy	Thu Dec 20 16:53:51 2001 +0100
+++ b/src/HOL/MicroJava/J/JListExample.thy	Thu Dec 20 17:08:55 2001 +0100
@@ -91,7 +91,7 @@
 *}
 
 generate_code
-  test = "query (example_prg\<turnstile>Norm (Map.empty, Map.empty)
+  test = "example_prg\<turnstile>Norm (Map.empty, Map.empty)
     -(Expr (l1_name::=NewC list_name);;
       Expr ({list_name}(LAcc l1_name)..val_name:=Lit (Intg 1));;
       Expr (l2_name::=NewC list_name);;
@@ -105,7 +105,7 @@
       Expr ({list_name}(LAcc l1_name)..
         append_name({[RefT (ClassT list_name)]}[LAcc l3_name]));;
       Expr ({list_name}(LAcc l1_name)..
-        append_name({[RefT (ClassT list_name)]}[LAcc l4_name])))-> s1)"
+        append_name({[RefT (ClassT list_name)]}[LAcc l4_name])))-> _"
 
 subsection {* Big step execution *}
 
diff -r 226873bffa3a -r 9df4b3934487 src/HOL/Tools/inductive_codegen.ML
--- a/src/HOL/Tools/inductive_codegen.ML	Thu Dec 20 16:53:51 2001 +0100
+++ b/src/HOL/Tools/inductive_codegen.ML	Thu Dec 20 17:08:55 2001 +0100
@@ -482,8 +482,8 @@
        None => None
      | Some (names, intrs) =>
          let
-          fun mk_mode (((ts, mode), i), Var _) = ((ts, mode), i+1)
-            | mk_mode (((ts, mode), i), Free _) = ((ts, mode), i+1)
+          fun mk_mode (((ts, mode), i), Const ("dummy_pattern", _)) =
+                ((ts, mode), i+1)
             | mk_mode (((ts, mode), i), t) = ((ts @ [t], mode @ [i]), i+1);
 
            val gr1 = mk_extra_defs thy
@@ -508,12 +508,11 @@
   | _ => None);
 
 fun inductive_codegen thy gr dep brack (Const ("op :", _) $ t $ u) =
-      (case mk_ind_call thy gr dep t u false of
+      ((case mk_ind_call thy gr dep (Term.no_dummy_patterns t) u false of
          None => None
        | Some (gr', call_p) => Some (gr', (if brack then parens else I)
            (Pretty.block [Pretty.str "?! (", call_p, Pretty.str ")"])))
-  | inductive_codegen thy gr dep brack (Free ("query", _) $ (Const ("op :", _) $ t $ u)) =
-      mk_ind_call thy gr dep t u true
+        handle TERM _ => mk_ind_call thy gr dep t u true)
   | inductive_codegen thy gr dep brack _ = None;
 
 val setup =