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