equal
deleted
inserted
replaced
790 datatype lhs_pat = |
790 datatype lhs_pat = |
791 Only_Vars |
791 Only_Vars |
792 | Prim_Pattern of string |
792 | Prim_Pattern of string |
793 | Any_Pattern; |
793 | Any_Pattern; |
794 |
794 |
795 fun is_likely_pat_complete ctxt props = |
795 fun is_apparently_pat_complete ctxt props = |
796 let |
796 let |
797 val is_Var_or_Bound = is_Var orf is_Bound; |
797 val is_Var_or_Bound = is_Var orf is_Bound; |
798 |
798 |
799 fun lhs_pat_of t = |
799 fun lhs_pat_of t = |
800 (case t of |
800 (case t of |
963 (case partition_props consts props of |
963 (case partition_props consts props of |
964 SOME propss => |
964 SOME propss => |
965 (props, |
965 (props, |
966 [IRec (map2 (fn const => fn props => |
966 [IRec (map2 (fn const => fn props => |
967 {const = const, props = props, |
967 {const = const, props = props, |
968 pat_complete = is_likely_pat_complete ctxt props}) |
968 pat_complete = is_apparently_pat_complete ctxt props}) |
969 consts propss)]) |
969 consts propss)]) |
970 | NONE => def_or_spec ()) |
970 | NONE => def_or_spec ()) |
971 else if member (op =) [Spec_Rules.Inductive, Spec_Rules.Co_Inductive] |
971 else if member (op =) [Spec_Rules.Inductive, Spec_Rules.Co_Inductive] |
972 classif then |
972 classif then |
973 if is_inductive_set_intro (hd props) then |
973 if is_inductive_set_intro (hd props) then |