# HG changeset patch
# User wenzelm
# Date 1565190007 -7200
# Node ID 63333b6a22c0e8878964f955d1dd8b95c7862cd8
# Parent  59250a32811356003cea2ca0e9c1a1555dde2c70
eliminated pointless comments;

diff -r 59250a328113 -r 63333b6a22c0 src/HOL/Tools/cnf.ML
--- a/src/HOL/Tools/cnf.ML	Wed Aug 07 15:49:33 2019 +0200
+++ b/src/HOL/Tools/cnf.ML	Wed Aug 07 17:00:07 2019 +0200
@@ -136,7 +136,6 @@
   let
     (* eliminates negated disjunctions from the i-th premise, possibly *)
     (* adding new premises, then continues with the (i+1)-th premise   *)
-    (* int -> Thm.thm -> Thm.thm *)
     fun not_disj_to_prem i thm =
       if i > Thm.nprems_of thm then
         thm
@@ -145,7 +144,6 @@
           (Seq.hd (REPEAT_DETERM (resolve_tac ctxt [clause2raw_not_disj] i) thm))
     (* moves all premises to hyps, i.e. "[...] |- A1 ==> ... ==> An ==> B" *)
     (* becomes "[..., A1, ..., An] |- B"                                   *)
-    (* Thm.thm -> Thm.thm *)
     fun prems_to_hyps thm =
       fold (fn cprem => fn thm' =>
         Thm.implies_elim thm' (Thm.assume cprem)) (cprems_of thm) thm
@@ -283,8 +281,6 @@
 (*      (True, respectively).                                                *)
 (* ------------------------------------------------------------------------- *)
 
-(* Theory.theory -> Term.term -> Thm.thm *)
-
 fun simp_True_False_thm thy (Const (\<^const_name>\<open>HOL.conj\<close>, _) $ x $ y) =
       let
         val thm1 = simp_True_False_thm thy x