src/Tools/isac/BaseDefinitions/termC.sml
changeset 60310 908c760f0def
parent 60309 70a1d102660d
child 60331 40eb8aa2b0d6
     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 =