Commit 49d19f1c2a11083f36099116818011ce026539df - cafeobj

Fix: missing in make-axiom-instance. tswd 4 years ago

1 changed file(s) with 16 addition(s) and 16 deletion(s). Raw diff Collapse all Expand all

+16

-16

thstuff/apply-tactic.lisp less more

2238	2238	;;; terms in resulting axiom must be ground terms.
2239	2239	;;;
2240	2240	(defun make-axiom-instance (module subst axiom &optional (label nil))
2241		;; (declare (type (or null string) label))
2242	2241	(flet ((make-proper-label (label)
2243	2242	(if (stringp label)
2244	2243	(intern label)
2245	2244	label)))
2246		(let ((new-axiom (rule-copy-canonicalized axiom module)))
2247		(if subst
2248		(apply-substitution-to-axiom (make-real-instanciation-subst subst
2249		(axiom-variables new-axiom))
2250		new-axiom
2251		(if label
2252		(make-proper-label label)
2253		'init)
2254		(if label
2255		nil
2256		t))
2257		(setf (rule-labels new-axiom) (if label
2258		(make-proper-label label)
2259		(cons (make-proper-label label) (rule-labels new-axiom)))))
2260		new-axiom)))
	2245	(with-in-module (module)
	2246	(let ((new-axiom (rule-copy-canonicalized axiom module)))
	2247	(if subst
	2248	(apply-substitution-to-axiom (make-real-instanciation-subst subst
	2249	(axiom-variables new-axiom))
	2250	new-axiom
	2251	(if label
	2252	(make-proper-label label)
	2253	'init)
	2254	(if label
	2255	nil
	2256	t))
	2257	(setf (rule-labels new-axiom) (if label
	2258	(make-proper-label label)
	2259	(cons (make-proper-label label) (rule-labels new-axiom)))))
	2260	new-axiom))))
2261	2261
2262	2262	;;; instanciate-axiom
2263	2263	;;;