# HG changeset patch
# User wenzelm
# Date 1452724675 -3600
# Node ID 3a578ee55bffcdebcbd5b2147976aae5688e059e
# Parent  1221f2a469450535f913714f05b00efc5f0ac8d0
removed dead code;

diff -r 1221f2a46945 -r 3a578ee55bff src/HOL/Library/positivstellensatz.ML
--- a/src/HOL/Library/positivstellensatz.ML	Wed Jan 13 23:25:18 2016 +0100
+++ b/src/HOL/Library/positivstellensatz.ML	Wed Jan 13 23:37:55 2016 +0100
@@ -316,8 +316,6 @@
   | Abs (_,_,_) => find_cterm p (Thm.dest_abs NONE t |> snd)
   | _ => raise CTERM ("find_cterm",[t]);
 
-    (* Some conversions-related stuff which has been forbidden entrance into Pure/conv.ML*)
-fun instantiate_cterm' ty tms = Drule.cterm_rule (Thm.instantiate' ty tms)
 fun is_comb t = (case Thm.term_of t of _ $ _ => true | _ => false);
 
 fun is_binop ct ct' = ct aconvc (Thm.dest_fun (Thm.dest_fun ct'))