# HG changeset patch
# User haftmann
# Date 1130513224 -7200
# Node ID 3f5d0acdfdbac4f2c79400b96746ea7eb869f60f
# Parent  23e6cfda8c4b8261f3c4848899e77f2e771f08bd
added extraction interface for code generator

diff -r 23e6cfda8c4b -r 3f5d0acdfdba src/HOL/Product_Type.thy
--- a/src/HOL/Product_Type.thy	Fri Oct 28 16:43:46 2005 +0200
+++ b/src/HOL/Product_Type.thy	Fri Oct 28 17:27:04 2005 +0200
@@ -787,19 +787,32 @@
   "snd"     ("snd")
 
 ML {*
-local
+
+signature PRODUCT_TYPE_CODEGEN =
+sig
+  val strip_abs: int -> term -> term list * term;
+end;
+
+structure ProductTypeCodegen : PRODUCT_TYPE_CODEGEN =
+struct
 
 fun strip_abs 0 t = ([], t)
   | strip_abs i (Abs (s, T, t)) =
-    let
-      val s' = Codegen.new_name t s;
-      val v = Free (s', T)
-    in apfst (cons v) (strip_abs (i-1) (subst_bound (v, t))) end
+      let
+        val s' = Codegen.new_name t s;
+        val v = Free (s', T)
+      in apfst (cons v) (strip_abs (i-1) (subst_bound (v, t))) end
   | strip_abs i (u as Const ("split", _) $ t) = (case strip_abs (i+1) t of
         (v :: v' :: vs, u) => (HOLogic.mk_prod (v, v') :: vs, u)
       | _ => ([], u))
   | strip_abs i t = ([], t);
 
+end;
+
+local
+
+open ProductTypeCodegen;
+
 fun let_codegen thy defs gr dep thyname brack t = (case strip_comb t of
     (t1 as Const ("Let", _), t2 :: t3 :: ts) =>
     let