src/HOL/Tools/cnf_funcs.ML
changeset 20547 796ae7fa1049
parent 20440 e6fe74eebda3
child 21576 8c11b1ce2f05
     1.1 --- a/src/HOL/Tools/cnf_funcs.ML	Fri Sep 15 20:08:38 2006 +0200
     1.2 +++ b/src/HOL/Tools/cnf_funcs.ML	Fri Sep 15 22:56:08 2006 +0200
     1.3 @@ -42,8 +42,8 @@
     1.4  
     1.5  	val weakening_tac : int -> Tactical.tactic  (* removes the first hypothesis of a subgoal *)
     1.6  
     1.7 -	val make_cnf_thm  : Theory.theory -> Term.term -> Thm.thm
     1.8 -	val make_cnfx_thm : Theory.theory -> Term.term ->  Thm.thm
     1.9 +	val make_cnf_thm  : theory -> Term.term -> Thm.thm
    1.10 +	val make_cnfx_thm : theory -> Term.term ->  Thm.thm
    1.11  	val cnf_rewrite_tac  : int -> Tactical.tactic  (* converts all prems of a subgoal to CNF *)
    1.12  	val cnfx_rewrite_tac : int -> Tactical.tactic  (* converts all prems of a subgoal to (almost) definitional CNF *)
    1.13  end;
    1.14 @@ -176,8 +176,6 @@
    1.15  (* inst_thm: instantiates a theorem with a list of terms                     *)
    1.16  (* ------------------------------------------------------------------------- *)
    1.17  
    1.18 -(* Theory.theory -> Term.term list -> Thm.thm -> Thm.thm *)
    1.19 -
    1.20  fun inst_thm thy ts thm =
    1.21  	instantiate' [] (map (SOME o cterm_of thy) ts) thm;
    1.22