src/HOL/Tools/Function/induction_scheme.ML
changeset 32765 3032c0308019
parent 32603 e08fdd615333
child 32950 5d5e123443b3
equal deleted inserted replaced
32764:690f9cccf232 32765:3032c0308019
   118           end
   118           end
   119 
   119 
   120       fun PT_of (SchemeBranch { xs, ...}) =
   120       fun PT_of (SchemeBranch { xs, ...}) =
   121             foldr1 HOLogic.mk_prodT (map snd xs)
   121             foldr1 HOLogic.mk_prodT (map snd xs)
   122 
   122 
   123       val ST = BalancedTree.make (uncurry SumTree.mk_sumT) (map PT_of branches)
   123       val ST = Balanced_Tree.make (uncurry SumTree.mk_sumT) (map PT_of branches)
   124     in
   124     in
   125       IndScheme {T=ST, cases=map mk_case cases', branches=branches }
   125       IndScheme {T=ST, cases=map mk_case cases', branches=branches }
   126     end
   126     end
   127 
   127 
   128 
   128