src/Tools/induct.ML
changeset 32188 005f9abae1e3
parent 32171 220abde9962b
child 32432 64f30bdd3ba1
     1.1 --- a/src/Tools/induct.ML	Sat Jul 25 10:31:27 2009 +0200
     1.2 +++ b/src/Tools/induct.ML	Sat Jul 25 12:43:45 2009 +0200
     1.3 @@ -568,7 +568,7 @@
     1.4  *)
     1.5  
     1.6  fun get_inductT ctxt insts =
     1.7 -  fold_rev multiply (insts |> map
     1.8 +  fold_rev (map_product cons) (insts |> map
     1.9        ((fn [] => NONE | ts => List.last ts) #>
    1.10          (fn NONE => TVar (("'a", 0), []) | SOME t => Term.fastype_of t) #>
    1.11          find_inductT ctxt)) [[]]