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 32342 3fabf5b5fc83
parent 32287 65d5c5b30747
child 32952 aeb1e44fbc19 
--- a/src/HOL/Tools/inductive_codegen.ML	Thu Jul 30 13:52:18 2009 +0200
+++ b/src/HOL/Tools/inductive_codegen.ML	Thu Jul 30 15:20:57 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_splits u
+      let val (r, Ts, fs) = HOLogic.strip_psplits u
       in case strip_comb r of
           (Const (s, T), ts) =>
             (case (get_clauses thy s, get_assoc_code thy (s, T)) of
isabelle