# HG changeset patch
# User krauss
# Date 1187634979 -7200
# Node ID 65fd09a7243f4e17fff072e51fa1b80799bd3422
# Parent  93d78fdeb55a99bce5aa9d865de134473f1d0823
issue a warning, when encountering redundant equations (covered by prece3ding clauses)

diff -r 93d78fdeb55a -r 65fd09a7243f src/HOL/Tools/function_package/fundef_datatype.ML
--- a/src/HOL/Tools/function_package/fundef_datatype.ML	Mon Aug 20 19:52:52 2007 +0200
+++ b/src/HOL/Tools/function_package/fundef_datatype.ML	Mon Aug 20 20:36:19 2007 +0200
@@ -233,6 +233,18 @@
       spec @ map (pair true) catchalls
     end
 
+fun warn_if_redundant ctxt origs tss =
+    let
+	fun msg t = "Ignoring redundant equation: " ^ quote (ProofContext.string_of_term ctxt t)
+
+	val (tss', _) = chop (length origs) tss
+	fun check ((_, t), []) = (Output.warning (msg t); [])
+	  | check ((_, t), s) = s
+    in
+	map check (origs ~~ tss')
+    end
+
+
 fun sequential_preproc (config as FundefConfig {sequential, ...}) flags ctxt fixes spec =
     let
       val enabled = sequential orelse exists I flags
@@ -245,12 +257,15 @@
                             
           val eqs = map the_single eqss
                     
-          val spliteqs = eqs
+          val feqs = eqs
                            |> tap (check_defs ctxt fixes) (* Standard checks *)
                            |> tap (map (check_pats ctxt))    (* More checks for sequential mode *)
                            |> curry op ~~ flags'
-                           |> add_catchall ctxt fixes   (* Completion *)
-                           |> FundefSplit.split_some_equations ctxt
+
+	  val compleqs = add_catchall ctxt fixes feqs   (* Completion *)
+
+	  val spliteqs = warn_if_redundant ctxt feqs
+					   (FundefSplit.split_some_equations ctxt compleqs)
 
           fun restore_spec thms =
               nas ~~ Library.take (length nas, Library.unflat spliteqs thms)