1.1 --- a/src/Tools/isac/BaseDefinitions/termC.sml Mon Jun 21 15:36:09 2021 +0200
1.2 +++ b/src/Tools/isac/BaseDefinitions/termC.sml Mon Jun 21 15:42:53 2021 +0200
1.3 @@ -429,8 +429,8 @@
1.4 fun perm lhs rhs = var_perm (lhs, rhs) andalso not (lhs aconv rhs) andalso not (is_Var lhs);
1.5
1.6
1.7 -fun pairT T1 T2 = Type ("*", [T1, T2]);
1.8 -fun PairT T1 T2 = ([T1, T2] ---> Type ("*", [T1, T2]));
1.9 +fun pairT T1 T2 = Type (\<^type_name>\<open>prod\<close>, [T1, T2]);
1.10 +fun PairT T1 T2 = ([T1, T2] ---> Type (\<^type_name>\<open>prod\<close>, [T1, T2]));
1.11 fun pairt t1 t2 = Const (\<^const_name>\<open>Pair\<close>, PairT (type_of t1) (type_of t2)) $ t1 $ t2;
1.12
1.13 fun mk_factroot op_(*=thy.sqrt*) T fact root =