diff -r 662e0fd39823 -r 9781e17dcc23 src/HOL/Tools/prop_logic.ML
--- 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