1.1 --- a/TFL/post.sml	Fri Mar 31 10:17:32 2000 +0200
     1.2 +++ b/TFL/post.sml	Fri Mar 31 10:23:15 2000 +0200
     1.3 @@ -39,11 +39,7 @@
     1.4     val defer : theory -> xstring
     1.5                    -> thm list 
     1.6                    -> string list -> theory * thm
     1.7 -(*
     1.8 -   val simplify_defn : simpset * thm list 
     1.9 -                        -> theory * (string * Prim.pattern list)
    1.10 -                        -> {rules:thm list, induct:thm, tcs:term list}
    1.11 -*)
    1.12 +
    1.13    end;
    1.14  
    1.15  

     2.1 --- a/TFL/tfl.sml	Fri Mar 31 10:17:32 2000 +0200
     2.2 +++ b/TFL/tfl.sml	Fri Mar 31 10:23:15 2000 +0200
     2.3 @@ -107,25 +107,19 @@
     2.4  
     2.5  
     2.6  (*---------------------------------------------------------------------------
     2.7 - * This datatype carries some information about the origin of a
     2.8 - * clause in a function definition.
     2.9 + * Each pattern carries with it a tag (i,b) where
    2.10 + * i is the clause it came from and
    2.11 + * b=true indicates that clause was given by the user
    2.12 + * (or is an instantiation of a user supplied pattern)
    2.13 + * b=false --> i = ~1
    2.14   *---------------------------------------------------------------------------*)
    2.15 -(*
    2.16 -datatype pattern = GIVEN   of term * int
    2.17 -                 | OMITTED of term * int
    2.18 -*)
    2.19 -(* True means the pattern was given by the user
    2.20 -   (or is an instantiation of a user supplied pattern)
    2.21 -*)
    2.22 +
    2.23  type pattern = term * (int * bool)
    2.24  
    2.25  fun pattern_map f (tm,x) = (f tm, x);
    2.26  
    2.27  fun pattern_subst theta = pattern_map (subst_free theta);
    2.28 -(*
    2.29 -fun dest_pattern (GIVEN (tm,i)) = ((GIVEN,i),tm)
    2.30 -  | dest_pattern (OMITTED (tm,i)) = ((OMITTED,i),tm);
    2.31 -*)
    2.32 +
    2.33  val pat_of = fst;
    2.34  val row_of_pat = fst o snd;
    2.35  val given = snd o snd;
    2.36 @@ -343,7 +337,8 @@
    2.37       val originals = map (row_of_pat o #2) rows
    2.38       val dummy = case (originals\\finals)
    2.39               of [] => ()
    2.40 -          | L => mk_functional_err ("The following rows are inaccessible: " ^
    2.41 +          | L => mk_functional_err
    2.42 + ("The following clauses are redundant (covered by preceding clauses): " ^
    2.43                     commas (map Int.toString L))
    2.44   in {functional = Abs(Sign.base_name fname, ftype,
    2.45  		      abstract_over (atom,