# HG changeset patch
# User berghofe
# Date 1120218897 -7200
# Node ID f19d58cfb47a92ca3141383f82801e85a21913ae
# Parent  208ebc9311f2c51350643559acfa685699558f1a
Adapted to new interface of code generator.

diff -r 208ebc9311f2 -r f19d58cfb47a src/HOL/List.thy
--- a/src/HOL/List.thy	Fri Jul 01 13:54:12 2005 +0200
+++ b/src/HOL/List.thy	Fri Jul 01 13:54:57 2005 +0200
@@ -2260,20 +2260,20 @@
 ML {*
 local
 
-fun list_codegen thy gr dep b t =
-  let val (gr', ps) = foldl_map (Codegen.invoke_codegen thy dep false)
+fun list_codegen thy defs gr dep thyname b t =
+  let val (gr', ps) = foldl_map (Codegen.invoke_codegen thy defs dep thyname false)
     (gr, HOLogic.dest_list t)
   in SOME (gr', Pretty.list "[" "]" ps) end handle TERM _ => NONE;
 
 fun dest_nibble (Const (s, _)) = int_of_nibble (unprefix "List.nibble.Nibble" s)
   | dest_nibble _ = raise Match;
 
-fun char_codegen thy gr dep b (Const ("List.char.Char", _) $ c1 $ c2) =
+fun char_codegen thy defs gr dep thyname b (Const ("List.char.Char", _) $ c1 $ c2) =
     (let val c = chr (dest_nibble c1 * 16 + dest_nibble c2)
      in if Symbol.is_printable c then SOME (gr, Pretty.quote (Pretty.str c))
        else NONE
      end handle Fail _ => NONE | Match => NONE)
-  | char_codegen thy gr dep b _ = NONE;
+  | char_codegen thy defs gr dep thyname b _ = NONE;
 
 in
 
diff -r 208ebc9311f2 -r f19d58cfb47a src/HOL/Product_Type.thy
--- a/src/HOL/Product_Type.thy	Fri Jul 01 13:54:12 2005 +0200
+++ b/src/HOL/Product_Type.thy	Fri Jul 01 13:54:57 2005 +0200
@@ -797,7 +797,8 @@
       | _ => ([], u))
   | strip_abs i t = ([], t);
 
-fun let_codegen thy gr dep brack (t as Const ("Let", _) $ _ $ _) =
+fun let_codegen thy defs gr dep thyname brack t = (case strip_comb t of
+    (t1 as Const ("Let", _), t2 :: t3 :: ts) =>
     let
       fun dest_let (l as Const ("Let", _) $ t $ u) =
           (case strip_abs 1 u of
@@ -806,38 +807,45 @@
         | dest_let t = ([], t);
       fun mk_code (gr, (l, r)) =
         let
-          val (gr1, pl) = Codegen.invoke_codegen thy dep false (gr, l);
-          val (gr2, pr) = Codegen.invoke_codegen thy dep false (gr1, r);
+          val (gr1, pl) = Codegen.invoke_codegen thy defs dep thyname false (gr, l);
+          val (gr2, pr) = Codegen.invoke_codegen thy defs dep thyname false (gr1, r);
         in (gr2, (pl, pr)) end
-    in case dest_let t of
+    in case dest_let (t1 $ t2 $ t3) of
         ([], _) => NONE
       | (ps, u) =>
           let
             val (gr1, qs) = foldl_map mk_code (gr, ps);
-            val (gr2, pu) = Codegen.invoke_codegen thy dep false (gr1, u)
+            val (gr2, pu) = Codegen.invoke_codegen thy defs dep thyname false (gr1, u);
+            val (gr3, pargs) = foldl_map
+              (Codegen.invoke_codegen thy defs dep thyname false) (gr2, ts)
           in
-            SOME (gr2, Pretty.blk (0, [Pretty.str "let ", Pretty.blk (0, List.concat
-                (separate [Pretty.str ";", Pretty.brk 1] (map (fn (pl, pr) =>
-                  [Pretty.block [Pretty.str "val ", pl, Pretty.str " =",
-                     Pretty.brk 1, pr]]) qs))),
-              Pretty.brk 1, Pretty.str "in ", pu,
-              Pretty.brk 1, Pretty.str "end"]))
+            SOME (gr3, Codegen.mk_app brack
+              (Pretty.blk (0, [Pretty.str "let ", Pretty.blk (0, List.concat
+                  (separate [Pretty.str ";", Pretty.brk 1] (map (fn (pl, pr) =>
+                    [Pretty.block [Pretty.str "val ", pl, Pretty.str " =",
+                       Pretty.brk 1, pr]]) qs))),
+                Pretty.brk 1, Pretty.str "in ", pu,
+                Pretty.brk 1, Pretty.str "end"])) pargs)
           end
     end
-  | let_codegen thy gr dep brack t = NONE;
+  | _ => NONE);
 
-fun split_codegen thy gr dep brack (t as Const ("split", _) $ _) =
-    (case strip_abs 1 t of
-       ([p], u) =>
-         let
-           val (gr1, q) = Codegen.invoke_codegen thy dep false (gr, p);
-           val (gr2, pu) = Codegen.invoke_codegen thy dep false (gr1, u)
-         in
-           SOME (gr2, Pretty.block [Pretty.str "(fn ", q, Pretty.str " =>",
-             Pretty.brk 1, pu, Pretty.str ")"])
-         end
-     | _ => NONE)
-  | split_codegen thy gr dep brack t = NONE;
+fun split_codegen thy defs gr dep thyname brack t = (case strip_comb t of
+    (t1 as Const ("split", _), t2 :: ts) =>
+      (case strip_abs 1 (t1 $ t2) of
+         ([p], u) =>
+           let
+             val (gr1, q) = Codegen.invoke_codegen thy defs dep thyname false (gr, p);
+             val (gr2, pu) = Codegen.invoke_codegen thy defs dep thyname false (gr1, u);
+             val (gr3, pargs) = foldl_map
+               (Codegen.invoke_codegen thy defs dep thyname false) (gr2, ts)
+           in
+             SOME (gr2, Codegen.mk_app brack
+               (Pretty.block [Pretty.str "(fn ", q, Pretty.str " =>",
+                 Pretty.brk 1, pu, Pretty.str ")"]) pargs)
+           end
+       | _ => NONE)
+  | _ => NONE);
 
 in