Removal of structure Context and its replacement by a theorem list of
congruence rules for use in CONTEXT_REWRITE_RULE (where definitions are
processed)

--- a/TFL/post.sml	Mon Jun 23 11:30:35 1997 +0200
+++ b/TFL/post.sml	Mon Jun 23 11:33:59 1997 +0200
@@ -23,7 +23,8 @@
    val define   : theory -> string -> string -> string list 
                   -> theory * Prim.pattern list
 
-   val simplify_defn : simpset -> theory * (string * Prim.pattern list)
+   val simplify_defn : simpset * thm list 
+                        -> theory * (string * Prim.pattern list)
                         -> {rules:thm list, induct:thm, tcs:term list}
 
   (*-------------------------------------------------------------------------
@@ -31,8 +32,6 @@
        val lazyR_def: theory -> term -> {theory:theory, eqns : thm}
    *-------------------------------------------------------------------------*)
 
-   val tflcongs : theory -> thm list
-
   end;
 
 
@@ -77,7 +76,6 @@
 			  (!claset addSDs [not0_implies_Suc] addss ss) 1),
     simplifier = Rules.simpl_conv ss []};
 
-fun tflcongs thy = Prim.Context.read() @ (#case_congs(Thry.extract_info thy));
 
 
 val concl = #2 o Rules.dest_thm;
@@ -185,14 +183,25 @@
 
 val wf_rel_defs = [lex_prod_def, measure_def, inv_image_def];
 
-fun simplify_defn ss (thy,(id,pats)) =
+(*Convert conclusion from = to ==*)
+val eq_reflect_list = map (fn th => (th RS eq_reflection) handle _ => th);
+
+(*---------------------------------------------------------------------------
+ * Install the basic context notions. Others (for nat and list and prod) 
+ * have already been added in thry.sml
+ *---------------------------------------------------------------------------*)
+val defaultTflCongs = eq_reflect_list [Thms.LET_CONG, if_cong];
+
+fun simplify_defn (ss, tflCongs) (thy,(id,pats)) =
    let val dummy = deny (id  mem  map ! (stamps_of_thy thy))
                         ("Recursive definition " ^ id ^ 
                          " would clash with the theory of the same name!")
        val def =  freezeT(get_def thy id)   RS   meta_eq_to_obj_eq
        val ss' = ss addsimps ((less_Suc_eq RS iffD2) :: wf_rel_defs)
        val {theory,rules,TCs,full_pats_TCs,patterns} = 
-                Prim.post_definition ss' (thy,(def,pats))
+                Prim.post_definition
+		   (ss', defaultTflCongs @ eq_reflect_list tflCongs)
+		   (thy, (def,pats))
        val {lhs=f,rhs} = S.dest_eq(concl def)
        val (_,[R,_]) = S.strip_comb rhs
        val {induction, rules, tcs} = 
@@ -243,14 +252,4 @@
  *
  *
  *---------------------------------------------------------------------------*)
-
-
-
-
-(*---------------------------------------------------------------------------
- * Install the basic context notions. Others (for nat and list and prod) 
- * have already been added in thry.sml
- *---------------------------------------------------------------------------*)
-val () = Prim.Context.write[Thms.LET_CONG, Thms.COND_CONG];
-
 end;

--- a/TFL/tfl.sig	Mon Jun 23 11:30:35 1997 +0200
+++ b/TFL/tfl.sig	Mon Jun 23 11:33:59 1997 +0200
@@ -17,7 +17,7 @@
 
    val wfrec_definition0 : theory -> string -> term -> term -> theory
 
-   val post_definition : simpset -> theory * (thm * pattern list)
+   val post_definition : simpset * thm list -> theory * (thm * pattern list)
 				 -> {theory : theory,
 				     rules  : thm, 
 				       TCs  : term list list,
@@ -25,7 +25,7 @@
 				  patterns  : pattern list}
 
 (*CURRENTLY UNUSED
-   val wfrec_eqns : theory -> term list
+   val wfrec_eqns : simpset * thm list -> theory -> term list
                      -> {WFR : term, 
                          proto_def : term,
                          extracta :(thm * term list) list,
@@ -46,10 +46,4 @@
                      -> theory 
                       -> {rules:thm, induction:thm, TCs:term list list}
                        -> {rules:thm, induction:thm, nested_tcs:thm list}
-
-   structure Context
-     : sig
-         val read : unit -> thm list
-         val write : thm list -> unit
-       end
 end;

--- a/TFL/tfl.sml	Mon Jun 23 11:30:35 1997 +0200
+++ b/TFL/tfl.sml	Mon Jun 23 11:33:59 1997 +0200
@@ -355,16 +355,9 @@
  * This structure keeps track of congruence rules that aren't derived
  * from a datatype definition.
  *---------------------------------------------------------------------------*)
-structure Context =
-struct
-  val non_datatype_context = ref []: thm list ref
-  fun read() = !non_datatype_context
-  fun write L = (non_datatype_context := L)
-end;
-
 fun extraction_thms thy = 
  let val {case_rewrites,case_congs} = Thry.extract_info thy
- in (case_rewrites, [e-mail]())
+ in (case_rewrites, case_congs)
  end;
 
 
@@ -393,7 +386,7 @@
   | givens (GIVEN(tm,_)::pats) = tm :: givens pats
   | givens (OMITTED _::pats)   = givens pats;
 
-fun post_definition ss (theory, (def, pats)) =
+fun post_definition (ss, tflCongs) (theory, (def, pats)) =
  let val tych = Thry.typecheck theory 
      val f = #lhs(S.dest_eq(concl def))
      val corollary = R.MATCH_MP Thms.WFREC_COROLLARY def
@@ -408,7 +401,7 @@
      val extract = R.CONTEXT_REWRITE_RULE 
 	             (ss, f, R,
 		      R.ISPECL (map tych [f,R]) Thms.CUT_LEMMA,
-		      context_congs)
+		      tflCongs@context_congs)
      val (rules, TCs) = ListPair.unzip (map extract corollaries')
      val rules0 = map (rewrite_rule [Thms.CUT_DEF]) rules
      val mk_cond_rule = R.FILTER_DISCH_ALL(not o curry (op aconv) WFR)
@@ -427,7 +420,7 @@
  * extraction commute for the non-nested case. For hol90 users, this 
  * function can be invoked without being in draft mode.
  * CURRENTLY UNUSED
-fun wfrec_eqns ss thy eqns =
+fun wfrec_eqns (ss, tflCongs) thy eqns =
  let val {functional,pats} = mk_functional thy eqns
      val given_pats = givens pats
      val {Bvar = f, Body} = S.dest_abs functional
@@ -448,7 +441,7 @@
      val extract = R.CONTEXT_REWRITE_RULE 
 	               (ss, f, R1, 
 		        R.ISPECL (map tych [f,R1]) Thms.CUT_LEMMA, 
-			context_congs)
+			tflCongs@context_congs)
  in {proto_def=proto_def, 
      WFR=WFR, 
      pats=pats,