src/Tools/induct.ML
changeset 35624 c4e29a0bb8c1
parent 35400 1fad91c02b98
child 35625 9c818cab0dd0
     1.1 --- a/src/Tools/induct.ML	Sat Mar 06 19:17:59 2010 +0000
     1.2 +++ b/src/Tools/induct.ML	Sun Mar 07 11:57:16 2010 +0100
     1.3 @@ -683,14 +683,14 @@
     1.4      fun add (SOME (_, (t, true))) ctxt = ((SOME t, []), ctxt)
     1.5        | add (SOME (SOME x, (t, _))) ctxt =
     1.6            let val ([(lhs, (_, th))], ctxt') =
     1.7 -            LocalDefs.add_defs [((x, NoSyn), (Thm.empty_binding, t))] ctxt
     1.8 +            Local_Defs.add_defs [((x, NoSyn), (Thm.empty_binding, t))] ctxt
     1.9            in ((SOME lhs, [th]), ctxt') end
    1.10        | add (SOME (NONE, (t as Free _, _))) ctxt = ((SOME t, []), ctxt)
    1.11        | add (SOME (NONE, (t, _))) ctxt =
    1.12            let
    1.13              val ([s], _) = Name.variants ["x"] (Variable.names_of ctxt);
    1.14              val ([(lhs, (_, th))], ctxt') =
    1.15 -              LocalDefs.add_defs [((Binding.name s, NoSyn),
    1.16 +              Local_Defs.add_defs [((Binding.name s, NoSyn),
    1.17                  (Thm.empty_binding, t))] ctxt
    1.18            in ((SOME lhs, [th]), ctxt') end
    1.19        | add NONE ctxt = ((NONE, []), ctxt);