--- 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]);