src/HOL/Tools/Function/induction_scheme.ML
changeset 32765 3032c0308019
parent 32603 e08fdd615333
child 32950 5d5e123443b3
--- a/src/HOL/Tools/Function/induction_scheme.ML	Tue Sep 29 22:33:27 2009 +0200
+++ b/src/HOL/Tools/Function/induction_scheme.ML	Tue Sep 29 22:48:24 2009 +0200
@@ -120,7 +120,7 @@
       fun PT_of (SchemeBranch { xs, ...}) =
             foldr1 HOLogic.mk_prodT (map snd xs)
 
-      val ST = BalancedTree.make (uncurry SumTree.mk_sumT) (map PT_of branches)
+      val ST = Balanced_Tree.make (uncurry SumTree.mk_sumT) (map PT_of branches)
     in
       IndScheme {T=ST, cases=map mk_case cases', branches=branches }
     end