# HG changeset patch
# User krauss
# Date 1188337987 -7200
# Node ID 619f78b717cb8ebd7517361bfd32ad27e4dffa6f
# Parent  70f0214b3ecce812b4167e477762747486a6217d
fixed pattern comnpletion; untabified

diff -r 70f0214b3ecc -r 619f78b717cb src/HOL/Tools/function_package/fundef_datatype.ML
--- a/src/HOL/Tools/function_package/fundef_datatype.ML	Tue Aug 28 20:13:47 2007 +0200
+++ b/src/HOL/Tools/function_package/fundef_datatype.ML	Tue Aug 28 23:53:07 2007 +0200
@@ -235,13 +235,13 @@
 
 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
+        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')
+        (map check (origs ~~ tss'); tss)
     end
 
 
@@ -262,10 +262,10 @@
                            |> tap (map (check_pats ctxt))    (* More checks for sequential mode *)
                            |> curry op ~~ flags'
 
-	  val compleqs = add_catchall ctxt fixes feqs   (* Completion *)
+    val compleqs = add_catchall ctxt fixes feqs   (* Completion *)
 
-	  val spliteqs = warn_if_redundant ctxt feqs
-					   (FundefSplit.split_some_equations ctxt compleqs)
+    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)