src/HOL/Tools/prop_logic.ML

   if is_cnf fm then fm
   else
     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 ()
             in
               (* Note that definitions are in NNF, but not CNF. *)

               val (fm2', defs2) = defcnf_or fm2
             in
               (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
       (* 'fm' must be a variable since the formula is in NNF *)
         | defcnf_from_nnf (Not fm) = Not fm