equal
deleted
inserted
replaced
11 signature METHOD_CLOSURE = |
11 signature METHOD_CLOSURE = |
12 sig |
12 sig |
13 val tag_free_thm: thm -> thm |
13 val tag_free_thm: thm -> thm |
14 val is_free_thm: thm -> bool |
14 val is_free_thm: thm -> bool |
15 val dummy_free_thm: thm |
15 val dummy_free_thm: thm |
16 val free_aware_rule_attribute: thm list -> (Context.generic -> thm -> thm) -> Thm.attribute |
|
17 val wrap_attribute: {handle_all_errs : bool, declaration : bool} -> |
16 val wrap_attribute: {handle_all_errs : bool, declaration : bool} -> |
18 Binding.binding -> theory -> theory |
17 Binding.binding -> theory -> theory |
19 val read: Proof.context -> Token.src -> Method.text |
18 val read: Proof.context -> Token.src -> Method.text |
20 val read_closure: Proof.context -> Token.src -> Method.text * Token.src |
19 val read_closure: Proof.context -> Token.src -> Method.text * Token.src |
21 val read_closure_input: Proof.context -> Input.source -> Method.text * Token.src |
20 val read_closure_input: Proof.context -> Input.source -> Method.text * Token.src |
75 |
74 |
76 val dummy_free_thm = tag_free_thm Drule.dummy_thm; |
75 val dummy_free_thm = tag_free_thm Drule.dummy_thm; |
77 |
76 |
78 fun is_free_thm thm = Properties.defined (Thm.get_tags thm) free_thmN; |
77 fun is_free_thm thm = Properties.defined (Thm.get_tags thm) free_thmN; |
79 |
78 |
80 fun free_aware_rule_attribute args f = |
|
81 Thm.rule_attribute (fn context => fn thm => |
|
82 if exists is_free_thm (thm :: args) then dummy_free_thm |
|
83 else f context thm); |
|
84 |
|
85 fun free_aware_attribute thy {handle_all_errs, declaration} src (context, thm) = |
79 fun free_aware_attribute thy {handle_all_errs, declaration} src (context, thm) = |
86 let |
80 let |
87 val src' = map Token.init_assignable src; |
81 val src' = map Token.init_assignable src; |
88 fun apply_att thm = (Attrib.attribute_global thy src') (context, thm); |
82 fun apply_att thm = (Attrib.attribute_global thy src') (context, thm); |
89 val _ = |
83 val _ = |