equal
deleted
inserted
replaced
666 |
666 |
667 fun trim_dependencies th deps = |
667 fun trim_dependencies th deps = |
668 if length deps > max_dependencies then NONE else SOME deps |
668 if length deps > max_dependencies then NONE else SOME deps |
669 |
669 |
670 fun isar_dependencies_of name_tabs th = |
670 fun isar_dependencies_of name_tabs th = |
671 let |
671 let val deps = thms_in_proof (SOME name_tabs) th in |
672 val deps = thms_in_proof (SOME name_tabs) th |
|
673 in |
|
674 if deps = [typedef_dep] orelse |
672 if deps = [typedef_dep] orelse |
675 deps = [class_some_dep] orelse |
673 deps = [class_some_dep] orelse |
676 exists (member (op =) fundef_ths) deps orelse |
674 exists (member (op =) fundef_ths) deps orelse |
677 exists (member (op =) typedef_ths) deps orelse |
675 exists (member (op =) typedef_ths) deps orelse |
678 is_size_def deps th then |
676 is_size_def deps th then |