src/Tools/induct.ML
changeset 43326 47cf4bc789aa
parent 43278 1fbdcebb364b
child 43333 2bdec7f430d3
     1.1 --- a/src/Tools/induct.ML	Thu Jun 09 17:46:25 2011 +0200
     1.2 +++ b/src/Tools/induct.ML	Thu Jun 09 17:51:49 2011 +0200
     1.3 @@ -692,7 +692,7 @@
     1.4        | add (SOME (NONE, (t as Free _, _))) ctxt = ((SOME t, []), ctxt)
     1.5        | add (SOME (NONE, (t, _))) ctxt =
     1.6            let
     1.7 -            val ([s], _) = Name.variants ["x"] (Variable.names_of ctxt);
     1.8 +            val (s, _) = Name.variant "x" (Variable.names_of ctxt);
     1.9              val ([(lhs, (_, th))], ctxt') =
    1.10                Local_Defs.add_defs [((Binding.name s, NoSyn),
    1.11                  (Thm.empty_binding, t))] ctxt