A version of guard-theorem that does no simplification.
This definition is based on
the definition of ACL2 source function
An advantage of not having the state argument is that this function can be called via magic-ev-fncall.
(defun guard-theorem-no-simplify (fn guard-debug wrld safe-mode gc-off) (cond ((not (getpropc fn 'unnormalized-body nil wrld)) *t*) (t (let ((names (or (getpropc fn 'recursivep nil wrld) (list fn)))) (mv-let (cl-set ttree) (guard-clauses-for-clique names guard-debug :do-not-simplify wrld safe-mode gc-off nil) (declare (ignore ttree)) (termify-clause-set cl-set))))))