changeset 14560 | 529464cffbfe |
parent 14250 | d09e92e7c2bf |
child 14859 | b4be6bdcbb94 |
--- a/src/HOL/Tools/inductive_codegen.ML Wed Apr 14 10:08:28 2004 +0200 +++ b/src/HOL/Tools/inductive_codegen.ML Wed Apr 14 11:44:57 2004 +0200 @@ -231,7 +231,7 @@ val in_vs = terms_vs in_ts; val concl_vs = terms_vs ts in - forall is_eqT (map snd (duplicates (flat (map term_vTs in_ts')))) andalso + forall is_eqT (map snd (duplicates (flat (map term_vTs in_ts)))) andalso (case check_mode_prems (arg_vs union in_vs) ps of None => false | Some vs => concl_vs subset vs)