src/Pure/Isar/theory_target.ML

--- a/src/Pure/Isar/theory_target.ML	Sun Oct 25 20:54:21 2009 +0100
+++ b/src/Pure/Isar/theory_target.ML	Sun Oct 25 21:35:46 2009 +0100
@@ -187,8 +187,8 @@
   in
     not (is_class andalso (similar_body orelse class_global)) ?
       (Context.mapping_result
-        (Sign.add_abbrev PrintMode.internal [] arg)
-        (ProofContext.add_abbrev PrintMode.internal [] arg)
+        (Sign.add_abbrev PrintMode.internal arg)
+        (ProofContext.add_abbrev PrintMode.internal arg)
       #-> (fn (lhs' as Const (d, _), _) =>
           similar_body ?
             (Context.mapping (Sign.revert_abbrev mode d) (ProofContext.revert_abbrev mode d) #>
@@ -214,13 +214,13 @@
                 if mx3 <> NoSyn then syntax_error c'
                 else LocalTheory.theory_result (Overloading.declare (c', U))
                   ##> Overloading.confirm b
-            | NONE => LocalTheory.theory_result (Sign.declare_const [] ((b, U), mx3))));
+            | NONE => LocalTheory.theory_result (Sign.declare_const ((b, U), mx3))));
     val (const, lthy') = lthy |> declare_const;
     val t = Term.list_comb (const, map Free xs);
   in
     lthy'
     |> is_locale ? term_syntax ta (locale_const ta Syntax.mode_default ((b, mx2), t))
-    |> is_class ? class_target ta (Class_Target.declare target [] ((b, mx1), t))
+    |> is_class ? class_target ta (Class_Target.declare target ((b, mx1), t))
     |> LocalDefs.add_def ((b, NoSyn), t)
   end;
 
@@ -241,17 +241,17 @@
   in
     lthy |>
      (if is_locale then
-        LocalTheory.theory_result (Sign.add_abbrev PrintMode.internal [] (b, global_rhs))
+        LocalTheory.theory_result (Sign.add_abbrev PrintMode.internal (b, global_rhs))
         #-> (fn (lhs, _) =>
           let val lhs' = Term.list_comb (Logic.unvarify lhs, xs) in
             term_syntax ta (locale_const ta prmode ((b, mx2), lhs')) #>
-            is_class ? class_target ta (Class_Target.abbrev target prmode [] ((b, mx1), t'))
+            is_class ? class_target ta (Class_Target.abbrev target prmode ((b, mx1), t'))
           end)
       else
         LocalTheory.theory
-          (Sign.add_abbrev (#1 prmode) [] (b, global_rhs) #-> (fn (lhs, _) =>
+          (Sign.add_abbrev (#1 prmode) (b, global_rhs) #-> (fn (lhs, _) =>
            Sign.notation true prmode [(lhs, mx3)])))
-    |> ProofContext.add_abbrev PrintMode.internal [] (b, t) |> snd
+    |> ProofContext.add_abbrev PrintMode.internal (b, t) |> snd
     |> LocalDefs.fixed_abbrev ((b, NoSyn), t)
   end;