diff options
| author | Josh Chen | 2020-07-28 14:24:22 +0200 |
|---|---|---|
| committer | Josh Chen | 2020-07-28 14:24:22 +0200 |
| commit | 2b0e14b16dcef0e829da95800b3c0af1975bb1ce (patch) | |
| tree | d11b2c8dadc6b5f2cdccfdab097c712d96e3500c | |
| parent | 6b27aa578257a6f4db9242b413a8008962b7f2e1 (diff) | |
small improvement
| -rw-r--r-- | spartan/core/elaborated_assumption.ML | 3 |
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))) |