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/function_package/mutual.ML
changeset 30906 3c7a76e79898
parent 30607 c3d1590debd8 
--- a/src/HOL/Tools/function_package/mutual.ML	Mon Apr 20 12:27:23 2009 +0200
+++ b/src/HOL/Tools/function_package/mutual.ML	Tue Apr 21 09:53:24 2009 +0200
@@ -87,12 +87,12 @@
       val num = length fs
         val fnames = map fst fs
         val fqgars = map (split_def ctxt) eqs
-        val arities = mk_arities fqgars
+        val arity_of = map (fn (fname,_,_,args,_) => (fname, length args)) fqgars
+                       |> AList.lookup (op =) #> the
 
         fun curried_types (fname, fT) =
             let
-              val k = the_default 1 (Symtab.lookup arities fname)
-              val (caTs, uaTs) = chop k (binder_types fT)
+              val (caTs, uaTs) = chop (arity_of fname) (binder_types fT)
             in
                 (caTs, uaTs ---> body_type fT)
             end
isabelle