TFL/tfl.sml

   end;
 
 
 
 (*---------------------------------------------------------------------------
- * This datatype carries some information about the origin of a
- * clause in a function definition.
- *---------------------------------------------------------------------------*)
-(*
-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)
-*)
+ * 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
+ *---------------------------------------------------------------------------*)
+
 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;
 
 (*---------------------------------------------------------------------------

      val patts2 = U.sort(fn p1=>fn p2=> row_of_pat p1 < row_of_pat p2) patts1
      val finals = map row_of_pat patts2
      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, 
 				     absfree(aname,atype, case_tm))),
      pats = patts2}