src/Pure/Isar/specification.ML
changeset 28941 128459bd72d2
parent 28880 f6a547c5dbbf
child 28965 1de908189869
     1.1 --- a/src/Pure/Isar/specification.ML	Mon Dec 01 16:02:57 2008 +0100
     1.2 +++ b/src/Pure/Isar/specification.ML	Mon Dec 01 19:41:16 2008 +0100
     1.3 @@ -190,7 +190,7 @@
     1.4              val y = Name.name_of b;
     1.5              val _ = x = y orelse
     1.6                error ("Head of definition " ^ quote x ^ " differs from declaration " ^ quote y ^
     1.7 -                Position.str_of (Name.pos_of b));
     1.8 +                Position.str_of (Binding.pos_of b));
     1.9            in (b, mx) end);
    1.10      val ((lhs, (_, th)), lthy2) = lthy |> LocalTheory.define Thm.definitionK
    1.11          (var, ((Name.map_name (suffix "_raw") name, []), rhs));
    1.12 @@ -223,7 +223,7 @@
    1.13              val y = Name.name_of b;
    1.14              val _ = x = y orelse
    1.15                error ("Head of abbreviation " ^ quote x ^ " differs from declaration " ^ quote y ^
    1.16 -                Position.str_of (Name.pos_of b));
    1.17 +                Position.str_of (Binding.pos_of b));
    1.18            in (b, mx) end);
    1.19      val lthy' = lthy
    1.20        |> ProofContext.set_syntax_mode mode    (* FIXME ?!? *)
    1.21 @@ -348,7 +348,7 @@
    1.22          lthy
    1.23          |> LocalTheory.notes kind (map2 (fn (a, _) => fn ths => (a, [(ths, [])])) stmt results')
    1.24          |> (fn (res, lthy') =>
    1.25 -          if Name.is_nothing name andalso null atts then
    1.26 +          if Binding.is_nothing name andalso null atts then
    1.27              (ProofDisplay.print_results true lthy' ((kind, ""), res); lthy')
    1.28            else
    1.29              let