Fixed bug in check_mode_clause.
authorberghofe
Wed Apr 14 11:44:57 2004 +0200 (2004-04-14)
changeset 14560529464cffbfe
parent 14559 7612d19d5638
child 14561 c53396af770e
Fixed bug in check_mode_clause.
src/HOL/Tools/inductive_codegen.ML
     1.1 --- a/src/HOL/Tools/inductive_codegen.ML	Wed Apr 14 10:08:28 2004 +0200
     1.2 +++ b/src/HOL/Tools/inductive_codegen.ML	Wed Apr 14 11:44:57 2004 +0200
     1.3 @@ -231,7 +231,7 @@
     1.4      val in_vs = terms_vs in_ts;
     1.5      val concl_vs = terms_vs ts
     1.6    in
     1.7 -    forall is_eqT (map snd (duplicates (flat (map term_vTs in_ts')))) andalso
     1.8 +    forall is_eqT (map snd (duplicates (flat (map term_vTs in_ts)))) andalso
     1.9      (case check_mode_prems (arg_vs union in_vs) ps of
    1.10         None => false
    1.11       | Some vs => concl_vs subset vs)