Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Tools/inductive_codegen.ML
changeset 32287 65d5c5b30747
parent 32091 30e2ffbba718
child 32342 3fabf5b5fc83 
--- a/src/HOL/Tools/inductive_codegen.ML	Wed Jul 29 16:43:02 2009 +0200
+++ b/src/HOL/Tools/inductive_codegen.ML	Wed Jul 29 16:48:34 2009 +0200
@@ -645,7 +645,7 @@
 
 fun inductive_codegen thy defs dep module brack t gr  = (case strip_comb t of
     (Const ("Collect", _), [u]) =>
-      let val (r, Ts, fs) = HOLogic.strip_split u
+      let val (r, Ts, fs) = HOLogic.strip_splits u
       in case strip_comb r of
           (Const (s, T), ts) =>
             (case (get_clauses thy s, get_assoc_code thy (s, T)) of
isabelle