aboutsummaryrefslogtreecommitdiff
path: root/spartan/core/goals.ML
diff options
context:
space:
mode:
Diffstat (limited to 'spartan/core/goals.ML')
-rw-r--r--spartan/core/goals.ML2
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