equal
deleted
inserted
replaced
48 val get = get_sg o Theory.sign_of; |
48 val get = get_sg o Theory.sign_of; |
49 val put = Theory.put_data kind Data; |
49 val put = Theory.put_data kind Data; |
50 |
50 |
51 end; |
51 end; |
52 |
52 |
53 (* FIXME deactivated due to Provers/classical.ML legacy code |
|
54 (*hide private data access functions*) |
53 (*hide private data access functions*) |
55 structure Sign: SIGN = Sign; |
54 structure Sign: SIGN = Sign; |
56 structure Theory: THEORY = Theory; |
55 structure Theory: THEORY = Theory; |
57 *) |
|