src/HOL/Tools/Function/mutual.ML
changeset 32765 3032c0308019
parent 32149 ef59550a55d3
child 33099 b8cdd3d73022
equal deleted inserted replaced
32764:690f9cccf232 32765:3032c0308019
   101         val argTs = map (foldr1 HOLogic.mk_prodT) caTss
   101         val argTs = map (foldr1 HOLogic.mk_prodT) caTss
   102 
   102 
   103         val dresultTs = distinct (op =) resultTs
   103         val dresultTs = distinct (op =) resultTs
   104         val n' = length dresultTs
   104         val n' = length dresultTs
   105 
   105 
   106         val RST = BalancedTree.make (uncurry SumTree.mk_sumT) dresultTs
   106         val RST = Balanced_Tree.make (uncurry SumTree.mk_sumT) dresultTs
   107         val ST = BalancedTree.make (uncurry SumTree.mk_sumT) argTs
   107         val ST = Balanced_Tree.make (uncurry SumTree.mk_sumT) argTs
   108 
   108 
   109         val fsum_type = ST --> RST
   109         val fsum_type = ST --> RST
   110 
   110 
   111         val ([fsum_var_name], _) = Variable.add_fixes [ defname ^ "_sum" ] ctxt
   111         val ([fsum_var_name], _) = Variable.add_fixes [ defname ^ "_sum" ] ctxt
   112         val fsum_var = (fsum_var_name, fsum_type)
   112         val fsum_var = (fsum_var_name, fsum_type)