changeset 18532 | 0347c1bba406 |
parent 18510 | 0a6c24f549c3 |
child 18629 | bdf01da93ed4 |
--- a/src/HOL/Tools/res_axioms.ML Sat Dec 31 21:49:39 2005 +0100 +++ b/src/HOL/Tools/res_axioms.ML Sat Dec 31 21:49:40 2005 +0100 @@ -347,7 +347,7 @@ fun rules_of_claset cs = let val {safeIs,safeEs,hazIs,hazEs,...} = rep_cs cs val intros = safeIs @ hazIs - val elims = safeEs @ hazEs + val elims = map Classical.classical_rule (safeEs @ hazEs) in debug ("rules_of_claset intros: " ^ Int.toString(length intros) ^ " elims: " ^ Int.toString(length elims));