aboutsummaryrefslogtreecommitdiff
path: root/spartan
diff options
context:
space:
mode:
authorJosh Chen2020-07-28 14:24:22 +0200
committerJosh Chen2020-07-28 14:24:22 +0200
commit2b0e14b16dcef0e829da95800b3c0af1975bb1ce (patch)
treed11b2c8dadc6b5f2cdccfdab097c712d96e3500c /spartan
parent6b27aa578257a6f4db9242b413a8008962b7f2e1 (diff)
small improvement
Diffstat (limited to '')
-rw-r--r--spartan/core/elaborated_assumption.ML3
1 files changed, 1 insertions, 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)))