equal
deleted
inserted
replaced
22 |
22 |
23 "----------- occurs_in -------------------------------------------"; |
23 "----------- occurs_in -------------------------------------------"; |
24 "----------- occurs_in -------------------------------------------"; |
24 "----------- occurs_in -------------------------------------------"; |
25 "----------- occurs_in -------------------------------------------"; |
25 "----------- occurs_in -------------------------------------------"; |
26 fun str2term str = (term_of o the o (parse thy )) str; |
26 fun str2term str = (term_of o the o (parse thy )) str; |
27 fun term2s t = Sign.string_of_term (sign_of thy) t; |
27 fun term2s t = Syntax.string_of_term (thy2ctxt thy) t; |
28 val t = str2term "x"; |
28 val t = str2term "x"; |
29 if occurs_in t t then "OK" else raise error "atools.sml: occurs_in x x -> f"; |
29 if occurs_in t t then "OK" else raise error "atools.sml: occurs_in x x -> f"; |
30 |
30 |
31 val t = str2term "x occurs_in x"; |
31 val t = str2term "x occurs_in x"; |
32 val SOME (str, t') = eval_occurs_in 0 "Atools.occurs'_in" t 0; |
32 val SOME (str, t') = eval_occurs_in 0 "Atools.occurs'_in" t 0; |