equal
deleted
inserted
replaced
1 (* Title: Pure/Isar/instance.ML |
|
2 ID: $Id$ |
|
3 Author: Florian Haftmann, TU Muenchen |
|
4 |
|
5 Wrapper for instantiation command. |
|
6 *) |
|
7 |
|
8 signature INSTANCE = |
|
9 sig |
|
10 val instantiation_cmd: xstring list * sort * xstring -> theory -> local_theory |
|
11 end; |
|
12 |
|
13 structure Instance : INSTANCE = |
|
14 struct |
|
15 |
|
16 fun read_multi_arity thy (raw_tycos, raw_sorts, raw_sort) = |
|
17 let |
|
18 val all_arities = map (fn raw_tyco => Sign.read_arity thy |
|
19 (raw_tyco, raw_sorts, raw_sort)) raw_tycos; |
|
20 val tycos = map #1 all_arities; |
|
21 val (_, sorts, sort) = hd all_arities; |
|
22 val vs = Name.names Name.context Name.aT sorts; |
|
23 in (tycos, vs, sort) end; |
|
24 |
|
25 fun instantiation_cmd raw_arities thy = |
|
26 TheoryTarget.instantiation (read_multi_arity thy raw_arities) thy; |
|
27 |
|
28 end; |
|