# HG changeset patch
# User berghofe
# Date 1061545902 -7200
# Node ID 5ffa75ce49191ab721e6fa154a9436b87a72233d
# Parent  f05f299512e914c8aae2d127428772418f768e24
Improved handling of modes for equality predicate, to avoid ill-typed
ML code due to comparisons between elements of function types.

diff -r f05f299512e9 -r 5ffa75ce4919 src/HOL/Tools/inductive_codegen.ML
--- a/src/HOL/Tools/inductive_codegen.ML	Thu Aug 21 16:20:45 2003 +0200
+++ b/src/HOL/Tools/inductive_codegen.ML	Fri Aug 22 11:51:42 2003 +0200
@@ -187,7 +187,10 @@
                 (iss ~~ args)))) (assoc' "modes" modes name))
 
   in (case strip_comb t of
-      (Const (name, _), args) => mk_modes name args
+      (Const ("op =", Type (_, [T, _])), _) =>
+        [Mode (([], [1]), []), Mode (([], [2]), [])] @
+        (if is_eqT T then [Mode (([], [1, 2]), [])] else [])
+    | (Const (name, _), args) => mk_modes name args
     | (Var ((name, _), _), args) => mk_modes name args
     | (Free (name, _), args) => mk_modes name args)
   end;
@@ -475,9 +478,7 @@
       val gr' = mk_extra_defs thy
         (Graph.add_edge (hd ids, dep)
           (Graph.new_node (hd ids, (None, "")) gr)) (hd ids) names intrs';
-      val (extra_modes', extra_factors) = lookup_modes gr' (hd ids);
-      val extra_modes =
-        ("op =", [([], [1]), ([], [2]), ([], [1, 2])]) :: extra_modes';
+      val (extra_modes, extra_factors) = lookup_modes gr' (hd ids);
       val fs = map (apsnd dest_factors)
         (foldl (add_prod_factors extra_factors) ([], flat (map (fn t =>
           Logic.strip_imp_concl t :: Logic.strip_imp_prems t) intrs')));