removed dead code;
authorwenzelm
Wed Jan 13 23:37:55 2016 +0100 (2016-01-13)
changeset 621773a578ee55bff
parent 62176 1221f2a46945
child 62178 c3c98ed94b0f
removed dead code;
src/HOL/Library/positivstellensatz.ML
     1.1 --- a/src/HOL/Library/positivstellensatz.ML	Wed Jan 13 23:25:18 2016 +0100
     1.2 +++ b/src/HOL/Library/positivstellensatz.ML	Wed Jan 13 23:37:55 2016 +0100
     1.3 @@ -316,8 +316,6 @@
     1.4    | Abs (_,_,_) => find_cterm p (Thm.dest_abs NONE t |> snd)
     1.5    | _ => raise CTERM ("find_cterm",[t]);
     1.6  
     1.7 -    (* Some conversions-related stuff which has been forbidden entrance into Pure/conv.ML*)
     1.8 -fun instantiate_cterm' ty tms = Drule.cterm_rule (Thm.instantiate' ty tms)
     1.9  fun is_comb t = (case Thm.term_of t of _ $ _ => true | _ => false);
    1.10  
    1.11  fun is_binop ct ct' = ct aconvc (Thm.dest_fun (Thm.dest_fun ct'))