# HG changeset patch
# User berghofe
# Date 1177507561 -7200
# Node ID 992222f3d2eb87aa2878e59292c94c3d1932a2e8
# Parent  e1cff9268177bf3edb9c18d6c66a6eb229c2443a
Moved function params_of to inductive_package.ML.

diff -r e1cff9268177 -r 992222f3d2eb src/HOL/Tools/inductive_codegen.ML
--- a/src/HOL/Tools/inductive_codegen.ML	Wed Apr 25 15:25:22 2007 +0200
+++ b/src/HOL/Tools/inductive_codegen.ML	Wed Apr 25 15:26:01 2007 +0200
@@ -16,17 +16,6 @@
 
 open Codegen;
 
-(* read off parameters of inductive predicate from raw induction rule *)
-fun params_of induct =
-  let
-    val (_ $ t $ u :: _) =
-      HOLogic.dest_conj (HOLogic.dest_Trueprop (concl_of induct));
-    val (_, ts) = strip_comb t;
-    val (_, us) = strip_comb u
-  in
-    List.take (ts, length ts - length us)
-  end;
-
 (**** theory data ****)
 
 fun merge_rules tabs =
@@ -77,7 +66,8 @@
             SOME k => k
           | NONE => (case rules of
              [] => (case try (InductivePackage.the_inductive (ProofContext.init thy)) s of
-                 SOME (_, {raw_induct, ...}) => length (params_of raw_induct)
+                 SOME (_, {raw_induct, ...}) =>
+                   length (InductivePackage.params_of raw_induct)
                | NONE => 0)
             | xs => snd (snd (snd (split_last xs)))))
         in CodegenData.put
@@ -97,7 +87,8 @@
       NONE => (case try (InductivePackage.the_inductive (ProofContext.init thy)) s of
         NONE => NONE
       | SOME ({names, ...}, {intrs, raw_induct, ...}) =>
-          SOME (names, thyname_of_const s thy, length (params_of raw_induct),
+          SOME (names, thyname_of_const s thy,
+            length (InductivePackage.params_of raw_induct),
             preprocess thy intrs))
     | SOME _ =>
         let