29 infix 1 ===; infix 1 ~= ; infix 1 <<; infix 1 ~<<; |
29 infix 1 ===; infix 1 ~= ; infix 1 <<; infix 1 ~<<; |
30 infix 9 ` ; infix 9 `% ; infix 9 `%%; infixr 9 oo; |
30 infix 9 ` ; infix 9 `% ; infix 9 `%%; infixr 9 oo; |
31 |
31 |
32 (* FIXME: use theory data for this *) |
32 (* FIXME: use theory data for this *) |
33 val copy_tab : string Symtab.table = |
33 val copy_tab : string Symtab.table = |
34 Symtab.make [(@{type_name "->"}, @{const_name "cfun_map"}), |
34 Symtab.make [(@{type_name cfun}, @{const_name "cfun_map"}), |
35 (@{type_name "++"}, @{const_name "ssum_map"}), |
35 (@{type_name ssum}, @{const_name "ssum_map"}), |
36 (@{type_name "**"}, @{const_name "sprod_map"}), |
36 (@{type_name sprod}, @{const_name "sprod_map"}), |
37 (@{type_name "*"}, @{const_name "cprod_map"}), |
37 (@{type_name "*"}, @{const_name "cprod_map"}), |
38 (@{type_name "u"}, @{const_name "u_map"})]; |
38 (@{type_name "u"}, @{const_name "u_map"})]; |
39 |
39 |
40 fun copy_of_dtyp tab r dt = |
40 fun copy_of_dtyp tab r dt = |
41 if Datatype_Aux.is_rec_type dt then copy tab r dt else ID |
41 if Datatype_Aux.is_rec_type dt then copy tab r dt else ID |