--- 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;