# HG changeset patch
# User paulson
# Date 935068417 -7200
# Node ID fcbf147e7b4c947e47ee6488ec980b5e2c0b8228
# Parent  52ea6848b908529229aa741d7f352f23f94320bd
removed needless comments

diff -r 52ea6848b908 -r fcbf147e7b4c TFL/tfl.sml
--- a/TFL/tfl.sml	Thu Aug 19 15:13:17 1999 +0200
+++ b/TFL/tfl.sml	Thu Aug 19 15:13:37 1999 +0200
@@ -493,10 +493,6 @@
      fun extract X = R.CONTEXT_REWRITE_RULE 
 	               (f, R1::SV, cut_apply, tflCongs@context_congs) X
  in {proto_def = proto_def,
-     (*LCP: want this??
-  (*Use == rather than = for definitions*)
-	 mk_const_def (Theory.sign_of thy) 
-	              (Name, Ty, S.rhs proto_def), *)
      SV=SV,
      WFR=WFR, 
      pats=pats,
@@ -516,7 +512,6 @@
 	   wfrec_eqns thy fid (congs tflCongs) eqns
      val R1 = S.rand WFR
      val f = #lhs(S.dest_eq proto_def)
-(*LCP: want this?     val f = #1 (Logic.dest_equals proto_def) *)
      val (extractants,TCl) = ListPair.unzip extracta
      val dummy = if !trace 
 		 then (writeln "Extractants = ";
@@ -537,13 +532,6 @@
      val (Name,Ty) = dest_atom c
      val defn = mk_const_def (Theory.sign_of thy) 
                  (Name, Ty, S.list_mk_abs (args,rhs)) 
-     (*LCP: want this??
-     val theory =
-       thy
-       |> PureThy.add_defs_i 
-            [Thm.no_attributes (fid ^ "_def", proto_def')];
-     val def = get_axiom theory (fid ^ "_def") RS meta_eq_to_obj_eq
-     *)
      val theory =
        thy
        |> PureThy.add_defs_i