equal
deleted
inserted
replaced
43 |
43 |
44 (* ext_subtype *) |
44 (* ext_subtype *) |
45 |
45 |
46 fun ext_subtype prep_term name (t, vs, mx) raw_set axms thms usr_tac thy = |
46 fun ext_subtype prep_term name (t, vs, mx) raw_set axms thms usr_tac thy = |
47 let |
47 let |
48 val _ = require_thy thy "Set" "subtype definitions"; |
48 val dummy = require_thy thy "Set" "subtype definitions"; |
49 val sign = sign_of thy; |
49 val sign = sign_of thy; |
50 |
50 |
51 (*rhs*) |
51 (*rhs*) |
52 val cset = prep_term sign raw_set; |
52 val cset = prep_term sign raw_set; |
53 val {T = setT, t = set, ...} = rep_cterm cset; |
53 val {T = setT, t = set, ...} = rep_cterm cset; |