improved tmp comment;
authorwenzelm
Fri, 25 Apr 1997 17:50:55 +0200
changeset 3061 25b2a895f864
parent 3060 7c3564de392e
child 3062 be354f68d340
improved tmp comment;
src/Pure/thm.ML
--- a/src/Pure/thm.ML	Fri Apr 25 17:28:43 1997 +0200
+++ b/src/Pure/thm.ML	Fri Apr 25 17:50:55 1997 +0200
@@ -95,7 +95,7 @@
   val concl_of          : thm -> term
   val cprop_of          : thm -> cterm
   val extra_shyps       : thm -> sort list
-  val force_strip_shyps : bool ref      (* FIXME tmp *)
+  val force_strip_shyps : bool ref      (* FIXME tmp (since 1995/08/01) *)
   val strip_shyps       : thm -> thm
   val implies_intr_shyps: thm -> thm
   val get_axiom         : theory -> string -> thm
@@ -488,7 +488,7 @@
 
 (* strip_shyps *)       (* FIXME improve? (e.g. only minimal extra sorts) *)
 
-val force_strip_shyps = ref true;  (* FIXME tmp *)
+val force_strip_shyps = ref true;  (* FIXME tmp (since 1995/08/01) *)
 
 (*remove extra sorts that are known to be syntactically non-empty*)
 fun strip_shyps thm =
@@ -502,7 +502,7 @@
          shyps =
          (if eq_set_sort (shyps',sorts) orelse 
              not (!force_strip_shyps) then shyps'
-          else    (* FIXME tmp *)
+          else    (* FIXME tmp (since 1995/08/01) *)
               (warning ("Removed sort hypotheses: " ^
                         commas (map Sorts.str_of_sort (shyps' \\ sorts)));
                warning "Let's hope these sorts are non-empty!";