src/Pure/thm.ML
changeset 3061 25b2a895f864
parent 3037 99ed078e6ae7
child 3410 98f59f455d57
     1.1 --- a/src/Pure/thm.ML	Fri Apr 25 17:28:43 1997 +0200
     1.2 +++ b/src/Pure/thm.ML	Fri Apr 25 17:50:55 1997 +0200
     1.3 @@ -95,7 +95,7 @@
     1.4    val concl_of          : thm -> term
     1.5    val cprop_of          : thm -> cterm
     1.6    val extra_shyps       : thm -> sort list
     1.7 -  val force_strip_shyps : bool ref      (* FIXME tmp *)
     1.8 +  val force_strip_shyps : bool ref      (* FIXME tmp (since 1995/08/01) *)
     1.9    val strip_shyps       : thm -> thm
    1.10    val implies_intr_shyps: thm -> thm
    1.11    val get_axiom         : theory -> string -> thm
    1.12 @@ -488,7 +488,7 @@
    1.13  
    1.14  (* strip_shyps *)       (* FIXME improve? (e.g. only minimal extra sorts) *)
    1.15  
    1.16 -val force_strip_shyps = ref true;  (* FIXME tmp *)
    1.17 +val force_strip_shyps = ref true;  (* FIXME tmp (since 1995/08/01) *)
    1.18  
    1.19  (*remove extra sorts that are known to be syntactically non-empty*)
    1.20  fun strip_shyps thm =
    1.21 @@ -502,7 +502,7 @@
    1.22           shyps =
    1.23           (if eq_set_sort (shyps',sorts) orelse 
    1.24               not (!force_strip_shyps) then shyps'
    1.25 -          else    (* FIXME tmp *)
    1.26 +          else    (* FIXME tmp (since 1995/08/01) *)
    1.27                (warning ("Removed sort hypotheses: " ^
    1.28                          commas (map Sorts.str_of_sort (shyps' \\ sorts)));
    1.29                 warning "Let's hope these sorts are non-empty!";