equal
deleted
inserted
replaced
32 val full = Sign.full_name (Theory.sign_of thy); |
32 val full = Sign.full_name (Theory.sign_of thy); |
33 |
33 |
34 fun arity_of (raw_name, args, mx) = |
34 fun arity_of (raw_name, args, mx) = |
35 (full (Syntax.type_name raw_name mx), replicate (length args) HOLogic.termS, HOLogic.termS); |
35 (full (Syntax.type_name raw_name mx), replicate (length args) HOLogic.termS, HOLogic.termS); |
36 in |
36 in |
37 thy |
37 if can (Theory.assert_super HOL.thy) thy then |
38 |> PureThy.add_typedecls decls |
38 thy |
39 |> Theory.add_arities_i (map arity_of decls) |
39 |> PureThy.add_typedecls decls |
|
40 |> Theory.add_arities_i (map arity_of decls) |
|
41 else thy |> PureThy.add_typedecls decls |
40 end; |
42 end; |
41 |
43 |
42 |
44 |
43 |
45 |
44 (** type definitions **) |
46 (** type definitions **) |