# 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