src/Provers/blast.ML
changeset 56245 84fc7dfa3cd4
parent 54943 1276861f2724
child 58826 2ed2eaabe3df
--- a/src/Provers/blast.ML	Fri Mar 21 15:12:03 2014 +0100
+++ b/src/Provers/blast.ML	Fri Mar 21 20:33:56 2014 +0100
@@ -419,11 +419,12 @@
 
 
 (* A1==>...An==>B  goes to  [A1,...,An], where B is not an implication *)
-fun strip_imp_prems (Const ("==>", _) $ A $ B) = strip_Trueprop A :: strip_imp_prems B
+fun strip_imp_prems (Const (@{const_name Pure.imp}, _) $ A $ B) =
+      strip_Trueprop A :: strip_imp_prems B
   | strip_imp_prems _ = [];
 
 (* A1==>...An==>B  goes to B, where B is not an implication *)
-fun strip_imp_concl (Const ("==>", _) $ A $ B) = strip_imp_concl B
+fun strip_imp_concl (Const (@{const_name Pure.imp}, _) $ A $ B) = strip_imp_concl B
   | strip_imp_concl A = strip_Trueprop A;
 
 
@@ -443,7 +444,7 @@
           else P :: delete_concl Ps
       | _ => P :: delete_concl Ps);
 
-fun skoPrem state vars (Const ("all", _) $ Abs (_, P)) =
+fun skoPrem state vars (Const (@{const_name Pure.all}, _) $ Abs (_, P)) =
         skoPrem state vars (subst_bound (Skolem (gensym state "S", vars), P))
   | skoPrem _ _ P = P;
 
@@ -1177,7 +1178,7 @@
 (*Make a list of all the parameters in a subgoal, even if nested*)
 local open Term
 in
-fun discard_foralls (Const("all",_)$Abs(a,T,t)) = discard_foralls t
+fun discard_foralls (Const(@{const_name Pure.all},_)$Abs(a,T,t)) = discard_foralls t
   | discard_foralls t = t;
 end;