# HG changeset patch
# User wenzelm
# Date 1452701108 -3600
# Node ID b61c55e4b4b92031628ee2ab48b47cf43a5df6e9
# Parent  a6047f511de7aa2da6e7bf7c2166abac1c25ed57
tuned;

diff -r a6047f511de7 -r b61c55e4b4b9 src/Pure/global_theory.ML
--- a/src/Pure/global_theory.ML	Wed Jan 13 16:55:56 2016 +0100
+++ b/src/Pure/global_theory.ML	Wed Jan 13 17:05:08 2016 +0100
@@ -189,13 +189,13 @@
   in ((name, thms), thy') end);
 
 
-(* store axioms as theorems *)
+(* old-style defs *)
 
 local
 
 fun add unchecked overloaded = fold_map (fn ((b, prop), atts) => fn thy =>
   let
-    val context as (ctxt, _) = Defs.global_context thy;
+    val context = Defs.global_context thy;
     val ((_, def), thy') = Thm.add_def context unchecked overloaded (b, prop) thy;
     val thm = def
       |> Thm.forall_intr_frees