src/Pure/Isar/class.ML
changeset 45293 57def0b39696
parent 45291 57cd50f98fdc
child 45310 adaf2184b79d
--- a/src/Pure/Isar/class.ML	Fri Oct 28 23:10:44 2011 +0200
+++ b/src/Pure/Isar/class.ML	Fri Oct 28 23:16:50 2011 +0200
@@ -560,7 +560,7 @@
         abbrev = Generic_Target.abbrev
           (fn prmode => fn (b, mx) => fn (t, _) => fn _ =>
             Generic_Target.theory_abbrev prmode ((b, mx), t)),
-        declaration = K Generic_Target.theory_declaration,
+        declaration = Generic_Target.theory_declaration o #syntax,
         pretty = pretty,
         exit = Local_Theory.target_of o conclude}
   end;