src/Pure/Isar/specification.ML
changeset 28862 53f13f763d4f
parent 28858 855e61829e22
child 28877 9ff624bd4fe1
     1.1 --- a/src/Pure/Isar/specification.ML	Thu Nov 20 14:55:25 2008 +0100
     1.2 +++ b/src/Pure/Isar/specification.ML	Thu Nov 20 14:55:28 2008 +0100
     1.3 @@ -269,8 +269,8 @@
     1.4        in ((prems, stmt, []), goal_ctxt) end
     1.5    | Element.Obtains obtains =>
     1.6        let
     1.7 -        val case_names = obtains |> map_index (fn (i, (binding, _)) =>
     1.8 -          let val name = Name.name_of binding
     1.9 +        val case_names = obtains |> map_index (fn (i, (b, _)) =>
    1.10 +          let val name = Name.name_of b
    1.11            in if name = "" then string_of_int (i + 1) else name end);
    1.12          val constraints = obtains |> map (fn (_, (vars, _)) =>
    1.13            Element.Constrains