equal
deleted
inserted
replaced
99 |
99 |
100 (**** check if a term contains only constructor functions ****) |
100 (**** check if a term contains only constructor functions ****) |
101 |
101 |
102 fun is_constrt thy = |
102 fun is_constrt thy = |
103 let |
103 let |
104 val cnstrs = List.concat (List.concat (map |
104 val cnstrs = flat (maps |
105 (map (fn (_, (_, _, cs)) => map (apsnd length) cs) o #descr o snd) |
105 (map (fn (_, (_, _, cs)) => map (apsnd length) cs) o #descr o snd) |
106 (Symtab.dest (Datatype.get_datatypes thy)))); |
106 (Symtab.dest (Datatype.get_all thy))); |
107 fun check t = (case strip_comb t of |
107 fun check t = (case strip_comb t of |
108 (Var _, []) => true |
108 (Var _, []) => true |
109 | (Const (s, _), ts) => (case AList.lookup (op =) cnstrs s of |
109 | (Const (s, _), ts) => (case AList.lookup (op =) cnstrs s of |
110 NONE => false |
110 NONE => false |
111 | SOME i => length ts = i andalso forall check ts) |
111 | SOME i => length ts = i andalso forall check ts) |