Changed name of raw definition.
authorberghofe
Thu May 10 15:50:28 2007 +0200 (2007-05-10)
changeset 229236384c43da028
parent 22922 66baa75eae06
child 22924 17f1d7af43bd
Changed name of raw definition.
src/Pure/Isar/specification.ML
     1.1 --- a/src/Pure/Isar/specification.ML	Thu May 10 15:49:31 2007 +0200
     1.2 +++ b/src/Pure/Isar/specification.ML	Thu May 10 15:50:28 2007 +0200
     1.3 @@ -127,8 +127,7 @@
     1.4        if x = x' then mx
     1.5        else error ("Head of definition " ^ quote x ^ " differs from declaration " ^ quote x'));
     1.6      val ((lhs, (_, th)), lthy2) = lthy
     1.7 -(*    |> LocalTheory.def ((x, mx), ((name ^ "_raw", []), rhs));  FIXME *)
     1.8 -      |> LocalTheory.def Thm.definitionK ((x, mx), ((name, []), rhs));
     1.9 +      |> LocalTheory.def Thm.definitionK ((x, mx), ((name ^ "_raw", []), rhs));
    1.10      val ((b, [th']), lthy3) = lthy2
    1.11        |> LocalTheory.note Thm.definitionK
    1.12            ((name, CodegenData.add_func_attr false :: atts), [prove lthy2 th]);