# HG changeset patch
# User berghofe
# Date 1178805028 -7200
# Node ID 6384c43da0283b235a752ebf8ce2146d113d9e97
# Parent  66baa75eae06f252e7ec805358b3be18ec859131
Changed name of raw definition.

diff -r 66baa75eae06 -r 6384c43da028 src/Pure/Isar/specification.ML
--- a/src/Pure/Isar/specification.ML	Thu May 10 15:49:31 2007 +0200
+++ b/src/Pure/Isar/specification.ML	Thu May 10 15:50:28 2007 +0200
@@ -127,8 +127,7 @@
       if x = x' then mx
       else error ("Head of definition " ^ quote x ^ " differs from declaration " ^ quote x'));
     val ((lhs, (_, th)), lthy2) = lthy
-(*    |> LocalTheory.def ((x, mx), ((name ^ "_raw", []), rhs));  FIXME *)
-      |> LocalTheory.def Thm.definitionK ((x, mx), ((name, []), rhs));
+      |> LocalTheory.def Thm.definitionK ((x, mx), ((name ^ "_raw", []), rhs));
     val ((b, [th']), lthy3) = lthy2
       |> LocalTheory.note Thm.definitionK
           ((name, CodegenData.add_func_attr false :: atts), [prove lthy2 th]);