From 2b0e14b16dcef0e829da95800b3c0af1975bb1ce Mon Sep 17 00:00:00 2001
From: Josh Chen
Date: Tue, 28 Jul 2020 14:24:22 +0200
Subject: small improvement

---
 spartan/core/elaborated_assumption.ML | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

diff --git a/spartan/core/elaborated_assumption.ML b/spartan/core/elaborated_assumption.ML
index e10a882..af3a384 100644
--- a/spartan/core/elaborated_assumption.ML
+++ b/spartan/core/elaborated_assumption.ML
@@ -436,8 +436,7 @@ val _ = Outer_Syntax.command \<^command_keyword>\<open>assuming\<close> "elabora
       val a' = map (fn (b, s, m) => (b, read_option_typ s, m)) a
       val b' = map (map read_terms) b
       val c' = c |> map (fn ((b, atts), ss) =>
-        ((b, map (Attrib.attribute ctxt o Attrib.check_src ctxt) atts),
-         map read_terms ss))
+        ((b, map (Attrib.attribute_cmd ctxt) atts), map read_terms ss))
       val c'' = elaborate ctxt c'
     in Proof.assume a' b' c'' state end)))
 
-- 
cgit v1.2.3