328 val normalize_eq_etc = normalize_eq o Term_Subst.zero_var_indexes |
328 val normalize_eq_etc = normalize_eq o Term_Subst.zero_var_indexes |
329 |
329 |
330 fun if_thm_before th th' = |
330 fun if_thm_before th th' = |
331 if Theory.subthy (pairself Thm.theory_of_thm (th, th')) then th else th' |
331 if Theory.subthy (pairself Thm.theory_of_thm (th, th')) then th else th' |
332 |
332 |
|
333 (* Hack: Conflate the facts about a class as seen from the outside with the |
|
334 corresponding low-level facts, so that MaSh can learn from the low-level |
|
335 proofs. *) |
|
336 fun un_class_ify s = |
|
337 case first_field "_class" s of |
|
338 SOME (pref, suf) => [s, pref ^ suf] |
|
339 | NONE => [s] |
|
340 |
333 fun build_all_names name_of facts = |
341 fun build_all_names name_of facts = |
334 let |
342 let |
335 fun cons_thm (_, th) = Termtab.cons_list (normalize_eq_etc (prop_of th), th) |
343 fun cons_thm (_, th) = Termtab.cons_list (normalize_eq_etc (prop_of th), th) |
336 fun add_alias canon alias = |
344 fun add_alias canon alias = |
337 Symtab.update (name_of alias, name_of (if_thm_before canon alias)) |
345 fold (fn s => Symtab.update (s, name_of (if_thm_before canon alias))) |
338 fun add_aliases (_, aliases as canon :: _) = fold (add_alias canon) aliases |
346 (un_class_ify (Thm.get_name_hint canon)) |
|
347 fun add_aliases (_, aliases as canon :: _) = |
|
348 fold (add_alias canon) aliases |
339 val tab = fold_rev cons_thm facts Termtab.empty |
349 val tab = fold_rev cons_thm facts Termtab.empty |
340 in Termtab.fold add_aliases tab Symtab.empty end |
350 in Termtab.fold add_aliases tab Symtab.empty end |
341 |
351 |
342 fun uniquify facts = |
352 fun uniquify facts = |
343 Termtab.fold (cons o snd) |
353 Termtab.fold (cons o snd) |