Moved function params_of to inductive_package.ML.
authorberghofe
Wed Apr 25 15:26:01 2007 +0200 (2007-04-25)
changeset 22791992222f3d2eb
parent 22790 e1cff9268177
child 22792 2443ae6dac7d
Moved function params_of to inductive_package.ML.
src/HOL/Tools/inductive_codegen.ML
     1.1 --- a/src/HOL/Tools/inductive_codegen.ML	Wed Apr 25 15:25:22 2007 +0200
     1.2 +++ b/src/HOL/Tools/inductive_codegen.ML	Wed Apr 25 15:26:01 2007 +0200
     1.3 @@ -16,17 +16,6 @@
     1.4  
     1.5  open Codegen;
     1.6  
     1.7 -(* read off parameters of inductive predicate from raw induction rule *)
     1.8 -fun params_of induct =
     1.9 -  let
    1.10 -    val (_ $ t $ u :: _) =
    1.11 -      HOLogic.dest_conj (HOLogic.dest_Trueprop (concl_of induct));
    1.12 -    val (_, ts) = strip_comb t;
    1.13 -    val (_, us) = strip_comb u
    1.14 -  in
    1.15 -    List.take (ts, length ts - length us)
    1.16 -  end;
    1.17 -
    1.18  (**** theory data ****)
    1.19  
    1.20  fun merge_rules tabs =
    1.21 @@ -77,7 +66,8 @@
    1.22              SOME k => k
    1.23            | NONE => (case rules of
    1.24               [] => (case try (InductivePackage.the_inductive (ProofContext.init thy)) s of
    1.25 -                 SOME (_, {raw_induct, ...}) => length (params_of raw_induct)
    1.26 +                 SOME (_, {raw_induct, ...}) =>
    1.27 +                   length (InductivePackage.params_of raw_induct)
    1.28                 | NONE => 0)
    1.29              | xs => snd (snd (snd (split_last xs)))))
    1.30          in CodegenData.put
    1.31 @@ -97,7 +87,8 @@
    1.32        NONE => (case try (InductivePackage.the_inductive (ProofContext.init thy)) s of
    1.33          NONE => NONE
    1.34        | SOME ({names, ...}, {intrs, raw_induct, ...}) =>
    1.35 -          SOME (names, thyname_of_const s thy, length (params_of raw_induct),
    1.36 +          SOME (names, thyname_of_const s thy,
    1.37 +            length (InductivePackage.params_of raw_induct),
    1.38              preprocess thy intrs))
    1.39      | SOME _ =>
    1.40          let