Inserted additional checks in functions dest_prem and add_prod_factors, to
authorberghofe
Wed Oct 29 19:18:15 2003 +0100 (2003-10-29)
changeset 14250d09e92e7c2bf
parent 14249 05382e257d95
child 14251 b91f632a1d37
Inserted additional checks in functions dest_prem and add_prod_factors, to
allow side conditions of the form "x : S", where S is not an inductive set.
src/HOL/Tools/inductive_codegen.ML
     1.1 --- a/src/HOL/Tools/inductive_codegen.ML	Wed Oct 29 16:16:20 2003 +0100
     1.2 +++ b/src/HOL/Tools/inductive_codegen.ML	Wed Oct 29 19:18:15 2003 +0100
     1.3 @@ -446,10 +446,11 @@
     1.4    let val ids = map (mk_const_id (sign_of thy)) names
     1.5    in Graph.add_edge (hd ids, dep) gr handle Graph.UNDEF _ =>
     1.6      let
     1.7 -      fun dest_prem factors (_ $ (Const ("op :", _) $ t $ u)) =
     1.8 +      fun dest_prem factors (_ $ (p as (Const ("op :", _) $ t $ u))) =
     1.9              (case head_of u of
    1.10 -               Const (name, _) => Prem (split_prod []
    1.11 -                 (the (assoc (factors, name))) t, u)
    1.12 +               Const (name, _) => (case assoc (factors, name) of
    1.13 +                   None => Sidecond p
    1.14 +                 | Some f => Prem (split_prod [] f t, u))
    1.15               | Var ((name, _), _) => Prem (split_prod []
    1.16                   (the (assoc (factors, name))) t, u))
    1.17          | dest_prem factors (_ $ ((eq as Const ("op =", _)) $ t $ u)) =
    1.18 @@ -467,8 +468,10 @@
    1.19          end;
    1.20  
    1.21        fun add_prod_factors extra_fs (fs, _ $ (Const ("op :", _) $ t $ u)) =
    1.22 -            infer_factors (sign_of thy) extra_fs
    1.23 -              (fs, (Some (FVar (prod_factors [] t)), u))
    1.24 +          (case apsome (get_clauses thy o fst) (try dest_Const (head_of u)) of
    1.25 +             Some None => fs
    1.26 +           | _ => infer_factors (sign_of thy) extra_fs
    1.27 +              (fs, (Some (FVar (prod_factors [] t)), u)))
    1.28          | add_prod_factors _ (fs, _) = fs;
    1.29  
    1.30        val intrs' = map (rename_term o #prop o rep_thm o standard) intrs;