1.1 --- a/src/Provers/induct_method.ML	Sat Oct 07 01:31:06 2006 +0200
     1.2 +++ b/src/Provers/induct_method.ML	Sat Oct 07 01:31:07 2006 +0200
     1.3 @@ -329,8 +329,8 @@
     1.4  fun add_defs def_insts =
     1.5    let
     1.6      fun add (SOME (SOME x, t)) ctxt =
     1.7 -          let val ((lhs, def), ctxt') = LocalDefs.add_def (x, t) ctxt
     1.8 -          in ((SOME (Free lhs), [def]), ctxt') end
     1.9 +          let val ([(lhs, (_, th))], ctxt') = LocalDefs.add_defs [((x, NoSyn), (("", []), t))] ctxt
    1.10 +          in ((SOME lhs, [th]), ctxt') end
    1.11        | add (SOME (NONE, t)) ctxt = ((SOME t, []), ctxt)
    1.12        | add NONE ctxt = ((NONE, []), ctxt);
    1.13    in fold_map add def_insts #> apfst (split_list #> apsnd flat) end;