diff -r 7d6b0241afab -r f191f25a5ec8 src/Pure/thm.ML
--- a/src/Pure/thm.ML	Mon Aug 14 13:42:27 1995 +0200
+++ b/src/Pure/thm.ML	Thu Aug 17 15:07:09 1995 +0200
@@ -465,7 +465,8 @@
 (** sort contexts **)
 
 (*account for lost sort constraints*)
-fun fix_shyps ths Ts th =
+fun fix_shyps ths Ts th = th;
+(* FIXME
   let
     fun thm_sorts (Thm {shyps, hyps, prop, ...}) =
       unions (shyps :: term_sorts prop :: map term_sorts hyps);
@@ -476,7 +477,7 @@
     Thm {sign = sign, maxidx = maxidx,
       shyps = lost_sorts @ shyps, hyps = hyps, prop = prop}
   end;
-
+*)
 (*remove sorts that are known to be non-empty (syntactically)*)
 val force_strip_shyps = ref true;  (* FIXME tmp *)
 fun strip_shyps th =