src/HOL/Tools/Function/fun.ML
changeset 48099 e7e647949c95
parent 46961 5c6955f487e5
child 49965 ee25a04fa06a
     1.1 --- a/src/HOL/Tools/Function/fun.ML	Wed Jun 06 10:35:05 2012 +0200
     1.2 +++ b/src/HOL/Tools/Function/fun.ML	Wed Jun 06 21:36:21 2012 +0200
     1.3 @@ -84,10 +84,10 @@
     1.4      spec @ mk_catchall fixes arity_of
     1.5    end
     1.6  
     1.7 -fun warnings ctxt origs tss =
     1.8 +fun further_checks ctxt origs tss =
     1.9    let
    1.10 -    fun warn_redundant t =
    1.11 -      warning ("Ignoring redundant equation: " ^ quote (Syntax.string_of_term ctxt t))
    1.12 +    fun fail_redundant t =
    1.13 +      error (cat_lines ["Equation is redundant (covered by preceding clauses):", Syntax.string_of_term ctxt t])
    1.14      fun warn_missing strs =
    1.15        warning (cat_lines ("Missing patterns in function definition:" :: strs))
    1.16  
    1.17 @@ -100,7 +100,7 @@
    1.18           @ ["(" ^ string_of_int (length rest) ^ " more)"])
    1.19  
    1.20      val _ = (origs ~~ tss')
    1.21 -      |> map (fn (t, ts) => if null ts then warn_redundant t else ())
    1.22 +      |> map (fn (t, ts) => if null ts then fail_redundant t else ())
    1.23    in
    1.24      ()
    1.25    end
    1.26 @@ -119,7 +119,7 @@
    1.27        val compleqs = add_catchall ctxt fixes feqs (* Completion *)
    1.28  
    1.29        val spliteqs = Function_Split.split_all_equations ctxt compleqs
    1.30 -        |> tap (warnings ctxt feqs)
    1.31 +        |> tap (further_checks ctxt feqs)
    1.32  
    1.33        fun restore_spec thms =
    1.34          bnds ~~ take (length bnds) (unflat spliteqs thms)