# HG changeset patch
# User wenzelm
# Date 935001581 -7200
# Node ID d55cd903c93da4b150370274f904f9d95edcf8f8
# Parent  2d09363ada6caac8eeb16fdc2d6214b0179cd542
(*no fix_shyps*);

diff -r 2d09363ada6c -r d55cd903c93d src/Pure/thm.ML
--- a/src/Pure/thm.ML	Wed Aug 18 19:17:29 1999 +0200
+++ b/src/Pure/thm.ML	Wed Aug 18 20:39:41 1999 +0200
@@ -1276,7 +1276,8 @@
 					       List.take(asms, m),
 					       concl))
 		   else raise THM("rotate_rule", k, [state])
-  in  Thm{sign_ref = sign_ref, 
+  in  (*no fix_shyps*)
+      Thm{sign_ref = sign_ref, 
 	  der = infer_derivs (Rotate_rule (k,i), [der]),
 	  maxidx = maxidx,
 	  shyps = shyps,
@@ -1303,7 +1304,8 @@
 					   List.take(moved_prems, m),
 					   concl)
 		   else raise THM("permute_prems:k", k, [rl])
-  in  Thm{sign_ref = sign_ref, 
+  in  (*no fix_shyps*)
+      Thm{sign_ref = sign_ref, 
 	  der = infer_derivs (Permute_prems (j,k), [der]),
 	  maxidx = maxidx,
 	  shyps = shyps,