Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
correcting alternative functions with tuples
authorbulwahn
Mon, 29 Mar 2010 17:30:54 +0200
changeset 36037 b1b21a8f6362
parent 36036 ea7d0df15be0
child 36038 385f706eff24
correcting alternative functions with tuples
src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Mon Mar 29 17:30:53 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Mon Mar 29 17:30:54 2010 +0200
@@ -1940,7 +1940,8 @@
         (case alternative_function_of (ProofContext.theory_of ctxt) name mode of
           SOME alt_function_name =>
             let
-              val (inpTs, outpTs) = split_modeT' mode (binder_types T)
+              val (inpTs, outpTs) = split_map_modeT (fn _ => fn T => (SOME T, NONE))
+                mode (binder_types T)
               val bs = map (pair "x") inpTs
               val bounds = map Bound (rev (0 upto (length bs) - 1))
               val f = Const (alt_function_name, inpTs ---> HOLogic.mk_tupleT outpTs)
isabelle