equal
deleted
inserted
replaced
82 val subgoal_count = Try.subgoal_count |
82 val subgoal_count = Try.subgoal_count |
83 |
83 |
84 fun reserved_isar_keyword_table () = |
84 fun reserved_isar_keyword_table () = |
85 Keyword.dest () |-> union (op =) |> map (rpair ()) |> Symtab.make |
85 Keyword.dest () |-> union (op =) |> map (rpair ()) |> Symtab.make |
86 |
86 |
87 (* FIXME: Similar yet different code in "mirabelle.ML". The code here has a few |
87 (* FIXME: Similar yet different code in "mirabelle.ML". The code here has a few fixes that seem to |
88 fixes that seem to be missing over there; or maybe the two code portions are |
88 be missing over there; or maybe the two code portions are not doing the same? *) |
89 not doing the same? *) |
|
90 fun fold_body_thm outer_name (map_plain_name, map_inclass_name) = |
89 fun fold_body_thm outer_name (map_plain_name, map_inclass_name) = |
91 let |
90 let |
92 fun app_thm map_name (_, (name, _, body)) accum = |
91 fun app_thm map_name (_, (name, _, body)) accum = |
93 let |
92 let |
94 val (anonymous, enter_class) = |
93 val (anonymous, enter_class) = |
102 accum |> app_body (if enter_class then map_inclass_name else map_name) (Future.join body) |
101 accum |> app_body (if enter_class then map_inclass_name else map_name) (Future.join body) |
103 else |
102 else |
104 accum |> union (op =) (the_list (map_name name)) |
103 accum |> union (op =) (the_list (map_name name)) |
105 end |
104 end |
106 and app_body map_name (PBody {thms, ...}) = fold (app_thm map_name) thms |
105 and app_body map_name (PBody {thms, ...}) = fold (app_thm map_name) thms |
107 in app_body map_plain_name end |
106 in |
|
107 app_body map_plain_name |
|
108 end |
108 |
109 |
109 fun thms_in_proof name_tabs th = |
110 fun thms_in_proof name_tabs th = |
110 let val map_names = (case name_tabs of SOME p => pairself Symtab.lookup p | NONE => `I SOME) in |
111 let val map_names = (case name_tabs of SOME p => pairself Symtab.lookup p | NONE => `I SOME) in |
111 fold_body_thm (Thm.get_name_hint th) map_names (Proofterm.strip_thm (Thm.proof_body_of th)) [] |
112 fold_body_thm (Thm.get_name_hint th) map_names (Proofterm.strip_thm (Thm.proof_body_of th)) [] |
112 end |
113 end |