--- a/src/HOL/Tools/prop_logic.ML Wed Feb 12 11:28:17 2014 +0100
+++ b/src/HOL/Tools/prop_logic.ML Wed Feb 12 13:31:18 2014 +0100
@@ -258,12 +258,9 @@
let
val fm' = nnf fm
(* 'new' specifies the next index that is available to introduce an auxiliary variable *)
- (* int ref *)
val new = Unsynchronized.ref (maxidx fm' + 1)
- (* unit -> int *)
fun new_idx () = let val idx = !new in new := idx+1; idx end
(* replaces 'And' by an auxiliary variable (and its definition) *)
- (* prop_formula -> prop_formula * prop_formula list *)
fun defcnf_or (And x) =
let
val i = new_idx ()
@@ -279,7 +276,6 @@
(Or (fm1', fm2'), defs1 @ defs2)
end
| defcnf_or fm = (fm, [])
- (* prop_formula -> prop_formula *)
fun defcnf_from_nnf True = True
| defcnf_from_nnf False = False
| defcnf_from_nnf (BoolVar i) = BoolVar i