aboutsummaryrefslogtreecommitdiff
path: root/spartan/core/elimination.ML
diff options
context:
space:
mode:
Diffstat (limited to 'spartan/core/elimination.ML')
-rw-r--r--spartan/core/elimination.ML2
1 files changed, 1 insertions, 1 deletions
diff --git a/spartan/core/elimination.ML b/spartan/core/elimination.ML
index cd4e414..cf9d21e 100644
--- a/spartan/core/elimination.ML
+++ b/spartan/core/elimination.ML
@@ -41,7 +41,7 @@ val _ = Theory.setup (
(Thm.declaration_attribute o register_rule))
""
#> Global_Theory.add_thms_dynamic (\<^binding>\<open>elim\<close>,
- fn context => (map #1 (rules (Context.proof_of context))))
+ fn context => map #1 (rules (Context.proof_of context)))
)