# HG changeset patch
# User berghofe
# Date 1081935897 -7200
# Node ID 529464cffbfed6fc0d1b75589d2a707090106ffd
# Parent  7612d19d5638ecae81c8e1914f7e00a8d40d6d22
Fixed bug in check_mode_clause.

diff -r 7612d19d5638 -r 529464cffbfe src/HOL/Tools/inductive_codegen.ML
--- 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)