diff options
| author | Josh Chen | 2020-07-31 18:10:10 +0200 |
|---|---|---|
| committer | Josh Chen | 2020-07-31 18:10:10 +0200 |
| commit | 77aa10763429d2ded040071fbf7bee331dd52f5e (patch) | |
| tree | 266abca73311031798c3936c1e44827bda292f25 /spartan/core/goals.ML | |
| parent | ff5454812f9e2720bd90c3a5437505644f63b487 (diff) | |
(REF) Tweak attribute names in preparation for new logical introduction rule behavior
Diffstat (limited to '')
| -rw-r--r-- | spartan/core/goals.ML | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/spartan/core/goals.ML b/spartan/core/goals.ML index 540f5c7..a04bd0e 100644 --- a/spartan/core/goals.ML +++ b/spartan/core/goals.ML @@ -151,7 +151,7 @@ fun gen_schematic_theorem map (apsnd (map (Local_Defs.fold new_lthy prf_tm_defs))) res in Local_Theory.notes_kind kind - [((name, @{attributes [typechk]} @ atts), + [((name, @{attributes [type]} @ atts), [(maps #2 res_folded, [])])] new_lthy end |