# HG changeset patch
# User nipkow
# Date 954490995 -7200
# Node ID a10ae360b63c0b1c3f5800608994de6fb0ccf1a0
# Parent  c3af577e7c7bcbbbba64021242da11a6d2e684b0
comments modified

diff -r c3af577e7c7b -r a10ae360b63c TFL/post.sml
--- a/TFL/post.sml	Fri Mar 31 10:17:32 2000 +0200
+++ b/TFL/post.sml	Fri Mar 31 10:23:15 2000 +0200
@@ -39,11 +39,7 @@
    val defer : theory -> xstring
                   -> thm list 
                   -> string list -> theory * thm
-(*
-   val simplify_defn : simpset * thm list 
-                        -> theory * (string * Prim.pattern list)
-                        -> {rules:thm list, induct:thm, tcs:term list}
-*)
+
   end;
 
 
diff -r c3af577e7c7b -r a10ae360b63c TFL/tfl.sml
--- a/TFL/tfl.sml	Fri Mar 31 10:17:32 2000 +0200
+++ b/TFL/tfl.sml	Fri Mar 31 10:23:15 2000 +0200
@@ -107,25 +107,19 @@
 
 
 (*---------------------------------------------------------------------------
- * This datatype carries some information about the origin of a
- * clause in a function definition.
+ * Each pattern carries with it a tag (i,b) where
+ * i is the clause it came from and
+ * b=true indicates that clause was given by the user
+ * (or is an instantiation of a user supplied pattern)
+ * b=false --> i = ~1
  *---------------------------------------------------------------------------*)
-(*
-datatype pattern = GIVEN   of term * int
-                 | OMITTED of term * int
-*)
-(* True means the pattern was given by the user
-   (or is an instantiation of a user supplied pattern)
-*)
+
 type pattern = term * (int * bool)
 
 fun pattern_map f (tm,x) = (f tm, x);
 
 fun pattern_subst theta = pattern_map (subst_free theta);
-(*
-fun dest_pattern (GIVEN (tm,i)) = ((GIVEN,i),tm)
-  | dest_pattern (OMITTED (tm,i)) = ((OMITTED,i),tm);
-*)
+
 val pat_of = fst;
 val row_of_pat = fst o snd;
 val given = snd o snd;
@@ -343,7 +337,8 @@
      val originals = map (row_of_pat o #2) rows
      val dummy = case (originals\\finals)
              of [] => ()
-          | L => mk_functional_err ("The following rows are inaccessible: " ^
+          | L => mk_functional_err
+ ("The following clauses are redundant (covered by preceding clauses): " ^
                    commas (map Int.toString L))
  in {functional = Abs(Sign.base_name fname, ftype,
 		      abstract_over (atom,