# HG changeset patch
# User wenzelm
# Date 861983455 -7200
# Node ID 25b2a895f86401aeb24c2094ae2dcdb846660953
# Parent  7c3564de392e23bd6c22992788f6959b14988fcd
improved tmp comment;

diff -r 7c3564de392e -r 25b2a895f864 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!";