# HG changeset patch
# User berghofe
# Date 1092157839 -7200
# Node ID 54ae6c6ef3b18b9e344d04d7c725f472f185107f
# Parent  5224130bc0d61e4dfe2c366bb18ef235ec172d93
Fixed bug in compile_clause that caused equality constraints
to be "forgotten".

diff -r 5224130bc0d6 -r 54ae6c6ef3b1 src/HOL/Tools/inductive_codegen.ML
--- a/src/HOL/Tools/inductive_codegen.ML	Mon Aug 09 15:27:27 2004 +0200
+++ b/src/HOL/Tools/inductive_codegen.ML	Tue Aug 10 19:10:39 2004 +0200
@@ -414,7 +414,7 @@
           let
             val vs' = distinct (flat (vs :: map term_vs out_ts));
             val Some (p, mode as Some (Mode ((_, js), _))) =
-              select_mode_prem thy modes' (arg_vs union vs') ps;
+              select_mode_prem thy modes' vs' ps;
             val ps' = filter_out (equal p) ps;
             val ((names', eqs), out_ts') =
               foldl_map check_constrt ((names, []), out_ts);
@@ -456,7 +456,7 @@
                  end)
           end;
 
-    val (gr', prem_p) = compile_prems in_ts' [] all_vs' gr ps;
+    val (gr', prem_p) = compile_prems in_ts' arg_vs all_vs' gr ps;
   in
     (gr', Pretty.block [Pretty.str "Seq.single inp :->", Pretty.brk 1, prem_p])
   end;