deactivated fix_shyps.
authornipkow
Thu, 17 Aug 1995 15:07:09 +0200
changeset 1229 f191f25a5ec8
parent 1228 7d6b0241afab
child 1230 87e29e18e970
deactivated fix_shyps.
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 =