src/HOL/Tools/inductive_codegen.ML
changeset 14163 5ffa75ce4919
parent 14162 f05f299512e9
child 14195 e7c9206dd2ef
     1.1 --- a/src/HOL/Tools/inductive_codegen.ML	Thu Aug 21 16:20:45 2003 +0200
     1.2 +++ b/src/HOL/Tools/inductive_codegen.ML	Fri Aug 22 11:51:42 2003 +0200
     1.3 @@ -187,7 +187,10 @@
     1.4                  (iss ~~ args)))) (assoc' "modes" modes name))
     1.5  
     1.6    in (case strip_comb t of
     1.7 -      (Const (name, _), args) => mk_modes name args
     1.8 +      (Const ("op =", Type (_, [T, _])), _) =>
     1.9 +        [Mode (([], [1]), []), Mode (([], [2]), [])] @
    1.10 +        (if is_eqT T then [Mode (([], [1, 2]), [])] else [])
    1.11 +    | (Const (name, _), args) => mk_modes name args
    1.12      | (Var ((name, _), _), args) => mk_modes name args
    1.13      | (Free (name, _), args) => mk_modes name args)
    1.14    end;
    1.15 @@ -475,9 +478,7 @@
    1.16        val gr' = mk_extra_defs thy
    1.17          (Graph.add_edge (hd ids, dep)
    1.18            (Graph.new_node (hd ids, (None, "")) gr)) (hd ids) names intrs';
    1.19 -      val (extra_modes', extra_factors) = lookup_modes gr' (hd ids);
    1.20 -      val extra_modes =
    1.21 -        ("op =", [([], [1]), ([], [2]), ([], [1, 2])]) :: extra_modes';
    1.22 +      val (extra_modes, extra_factors) = lookup_modes gr' (hd ids);
    1.23        val fs = map (apsnd dest_factors)
    1.24          (foldl (add_prod_factors extra_factors) ([], flat (map (fn t =>
    1.25            Logic.strip_imp_concl t :: Logic.strip_imp_prems t) intrs')));