equal
deleted
inserted
replaced
47 in add_parent thy [] end |
47 in add_parent thy [] end |
48 |
48 |
49 val thy_name_of_fact = hd o Long_Name.explode |
49 val thy_name_of_fact = hd o Long_Name.explode |
50 fun thy_of_fact thy = Context.this_theory thy o thy_name_of_fact |
50 fun thy_of_fact thy = Context.this_theory thy o thy_name_of_fact |
51 |
51 |
52 val all_names = |
52 val all_names = map (rpair () o nickname_of) #> Symtab.make |
53 filter_out is_likely_tautology_or_too_meta |
|
54 #> map (rpair () o nickname_of) #> Symtab.make |
|
55 |
53 |
56 fun generate_accessibility thy include_thy file_name = |
54 fun generate_accessibility thy include_thy file_name = |
57 let |
55 let |
58 val path = file_name |> Path.explode |
56 val path = file_name |> Path.explode |
59 val _ = File.write path "" |
57 val _ = File.write path "" |