changeset 30211 | 556d1810cdad |
parent 29581 | b3b33e0298eb |
child 30510 | 4120fc59dd85 |
--- a/src/Tools/induct.ML Tue Mar 03 14:07:23 2009 +0100 +++ b/src/Tools/induct.ML Tue Mar 03 14:07:43 2009 +0100 @@ -552,7 +552,7 @@ let fun add (SOME (SOME x, t)) ctxt = let val ([(lhs, (_, th))], ctxt') = - LocalDefs.add_defs [((x, NoSyn), ((Binding.empty, []), t))] ctxt + LocalDefs.add_defs [((x, NoSyn), (Thm.empty_binding, t))] ctxt in ((SOME lhs, [th]), ctxt') end | add (SOME (NONE, t)) ctxt = ((SOME t, []), ctxt) | add NONE ctxt = ((NONE, []), ctxt);