--- 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