src/HOL/Tools/Function/fun.ML
changeset 39276 2ad95934521f
parent 36960 01594f816e3a
child 41114 f9ae7c2abf7e
     1.1 --- a/src/HOL/Tools/Function/fun.ML	Fri Sep 10 10:59:10 2010 +0200
     1.2 +++ b/src/HOL/Tools/Function/fun.ML	Fri Sep 10 14:37:57 2010 +0200
     1.3 @@ -44,7 +44,7 @@
     1.4           ())
     1.5        end
     1.6  
     1.7 -    val (_, qs, gs, args, _) = split_def ctxt geq
     1.8 +    val (_, qs, gs, args, _) = split_def ctxt (K true) geq
     1.9  
    1.10      val _ = if not (null gs) then err "Conditional equations" else ()
    1.11      val _ = map check_constr_pattern args
    1.12 @@ -76,7 +76,7 @@
    1.13    end
    1.14  
    1.15  fun add_catchall ctxt fixes spec =
    1.16 -  let val fqgars = map (split_def ctxt) spec
    1.17 +  let val fqgars = map (split_def ctxt (K true)) spec
    1.18        val arity_of = map (fn (fname,_,_,args,_) => (fname, length args)) fqgars
    1.19                       |> AList.lookup (op =) #> the
    1.20    in