equal
deleted
inserted
replaced
54 |
54 |
55 (* must be exported in code.ML *) |
55 (* must be exported in code.ML *) |
56 fun is_constr thy = is_some o Code.get_datatype_of_constr thy; |
56 fun is_constr thy = is_some o Code.get_datatype_of_constr thy; |
57 |
57 |
58 (* Table from constant name (string) to term of inductive predicate *) |
58 (* Table from constant name (string) to term of inductive predicate *) |
59 structure Pred_Compile_Preproc = TheoryDataFun |
59 structure Pred_Compile_Preproc = Theory_Data |
60 ( |
60 ( |
61 type T = string Symtab.table; |
61 type T = string Symtab.table; |
62 val empty = Symtab.empty; |
62 val empty = Symtab.empty; |
63 val copy = I; |
|
64 val extend = I; |
63 val extend = I; |
65 fun merge _ = Symtab.merge (op =); |
64 fun merge data : T = Symtab.merge (op =) data; (* FIXME handle Symtab.DUP ?? *) |
66 ) |
65 ) |
67 |
66 |
68 fun pred_of_function thy name = Symtab.lookup (Pred_Compile_Preproc.get thy) name |
67 fun pred_of_function thy name = Symtab.lookup (Pred_Compile_Preproc.get thy) name |
69 |
68 |
70 fun defined thy = Symtab.defined (Pred_Compile_Preproc.get thy) |
69 fun defined thy = Symtab.defined (Pred_Compile_Preproc.get thy) |